algstr_4.miz
begin
registration
let X be
set;
let f be
sequence of X;
let n be
Nat;
cluster (f
| n) ->
Sequence-like;
correctness
proof
per cases ;
suppose
A1: X
<>
{} ;
n
c=
NAT ;
then n
c= (
dom f) by
A1,
FUNCT_2:def 1;
then (
dom (f
| n)) is
ordinal by
RELAT_1: 62;
hence thesis by
ORDINAL1:def 7;
end;
suppose X
=
{} ;
then f
=
{} ;
hence thesis;
end;
end;
end
definition
let X,x be
set;
::
ALGSTR_4:def1
func
IFXFinSequence (x,X) ->
XFinSequence of X equals
:
Def1: x if x is
XFinSequence of X
otherwise (
<%> X);
correctness ;
end
definition
let X be non
empty
set;
let f be
Function of (X
^omega ), X;
let c be
XFinSequence of X;
:: original:
.
redefine
func f
. c ->
Element of X ;
correctness
proof
c
in (X
^omega ) by
AFINSQ_1:def 7;
hence thesis by
FUNCT_2: 5;
end;
end
theorem ::
ALGSTR_4:1
Th1: for X,Y,Z be
set st Y
c= (
the_universe_of X) & Z
c= (
the_universe_of X) holds
[:Y, Z:]
c= (
the_universe_of X)
proof
let X,Y,Z be
set;
assume Y
c= (
the_universe_of X);
then
A1: Y
c= (
Tarski-Class (
the_transitive-closure_of X)) by
YELLOW_6:def 1;
assume Z
c= (
the_universe_of X);
then Z
c= (
Tarski-Class (
the_transitive-closure_of X)) by
YELLOW_6:def 1;
then
[:Y, Z:]
c= (
Tarski-Class (
the_transitive-closure_of X)) by
A1,
CLASSES1: 28;
hence
[:Y, Z:]
c= (
the_universe_of X) by
YELLOW_6:def 1;
end;
scheme ::
ALGSTR_4:sch1
FuncRecursiveUniq { F(
set) ->
set , F1,F2() ->
Function } :
F1()
= F2()
provided
A1: (
dom F1())
=
NAT & for n be
Nat holds (F1()
. n)
= F(|)
and
A2: (
dom F2())
=
NAT & for n be
Nat holds (F2()
. n)
= F(|);
reconsider L1 = F1() as
Sequence by
A1,
ORDINAL1:def 7;
reconsider L2 = F2() as
Sequence by
A2,
ORDINAL1:def 7;
A3: (
dom L1)
=
NAT & for B be
Ordinal, T1 be
Sequence st B
in
NAT & T1
= (L1
| B) holds (L1
. B)
= F(T1) by
A1;
A4: (
dom L2)
=
NAT & for B be
Ordinal, T2 be
Sequence st B
in
NAT & T2
= (L2
| B) holds (L2
. B)
= F(T2) by
A2;
L1
= L2 from
ORDINAL1:sch 3(
A3,
A4);
hence thesis;
end;
scheme ::
ALGSTR_4:sch2
FuncRecursiveExist { F(
set) ->
set } :
ex f be
Function st (
dom f)
=
NAT & for n be
Nat holds (f
. n)
= F(|);
consider L be
Sequence such that
A1: (
dom L)
=
NAT and
A2: for B be
Ordinal, L1 be
Sequence st B
in
NAT & L1
= (L
| B) holds (L
. B)
= F(L1) from
ORDINAL1:sch 4;
take L;
thus (
dom L)
=
NAT by
A1;
let n be
Nat;
reconsider B = n as
Ordinal;
B
in
NAT by
ORDINAL1:def 12;
then (L
. B)
= F(|) by
A2;
hence thesis;
end;
scheme ::
ALGSTR_4:sch3
FuncRecursiveUniqu2 { X() -> non
empty
set , F(
XFinSequence of X()) ->
Element of X() , F1,F2() ->
sequence of X() } :
F1()
= F2()
provided
A1: for n be
Nat holds (F1()
. n)
= F(|)
and
A2: for n be
Nat holds (F2()
. n)
= F(|);
deffunc
FX(
set) = F(IFXFinSequence);
reconsider f1 = F1() as
Function;
reconsider f2 = F2() as
Function;
A3: (
dom f1)
=
NAT & for n be
Nat holds (f1
. n)
=
FX(|)
proof
thus (
dom f1)
=
NAT by
FUNCT_2:def 1;
let n be
Nat;
thus (f1
. n)
= F(|) by
A1
.=
FX(|) by
Def1;
end;
A4: (
dom f2)
=
NAT & for n be
Nat holds (f2
. n)
=
FX(|)
proof
thus (
dom f2)
=
NAT by
FUNCT_2:def 1;
let n be
Nat;
thus (f2
. n)
= F(|) by
A2
.=
FX(|) by
Def1;
end;
f1
= f2 from
FuncRecursiveUniq(
A3,
A4);
hence thesis;
end;
scheme ::
ALGSTR_4:sch4
FuncRecursiveExist2 { X() -> non
empty
set , F(
XFinSequence of X()) ->
Element of X() } :
ex f be
sequence of X() st for n be
Nat holds (f
. n)
= F(|);
deffunc
FX(
set) = F(IFXFinSequence);
consider f be
Function such that
A1: (
dom f)
=
NAT and
A2: for n be
Nat holds (f
. n)
=
FX(|) from
FuncRecursiveExist;
for y be
object st y
in (
rng f) holds y
in X()
proof
let y be
object;
assume y
in (
rng f);
then
consider x be
object such that
A3: x
in (
dom f) & y
= (f
. x) by
FUNCT_1:def 3;
reconsider x as
Nat by
A1,
A3;
y
= F(IFXFinSequence) by
A3,
A2;
hence y
in X();
end;
then (
rng f)
c= X();
then
reconsider f9 = f as
sequence of X() by
A1,
FUNCT_2: 2;
take f9;
let n be
Nat;
(f
. n)
= F(IFXFinSequence) by
A2
.= F(|) by
Def1;
hence thesis;
end;
definition
let f,g be
Function;
::
ALGSTR_4:def2
pred f
extends g means (
dom g)
c= (
dom f) & f
tolerates g;
end
registration
cluster
empty for
multMagma;
existence
proof
take
multMagma (#
{} , the
BinOp of
{} #);
thus thesis;
end;
end
begin
definition
let M be
multMagma;
let R be
Equivalence_Relation of M;
::
ALGSTR_4:def3
attr R is
compatible means
:
Def3: for v,v9,w,w9 be
Element of M st v
in (
Class (R,v9)) & w
in (
Class (R,w9)) holds (v
* w)
in (
Class (R,(v9
* w9)));
end
registration
let M be
multMagma;
cluster (
nabla the
carrier of M) ->
compatible;
correctness
proof
set R = (
nabla the
carrier of M);
let v,v9,w,w9 be
Element of M;
assume v
in (
Class (R,v9)) & w
in (
Class (R,w9));
then
A1: M is non
empty;
then (
Class (R,(v9
* w9)))
= the
carrier of M by
EQREL_1: 26;
hence thesis by
A1,
SUBSET_1:def 1;
end;
end
registration
let M be
multMagma;
cluster
compatible for
Equivalence_Relation of M;
correctness
proof
take (
nabla the
carrier of M);
thus thesis;
end;
end
theorem ::
ALGSTR_4:2
Th2: for M be
multMagma, R be
Equivalence_Relation of M holds R is
compatible iff for v,v9,w,w9 be
Element of M st (
Class (R,v))
= (
Class (R,v9)) & (
Class (R,w))
= (
Class (R,w9)) holds (
Class (R,(v
* w)))
= (
Class (R,(v9
* w9)))
proof
let M be
multMagma;
let R be
Equivalence_Relation of M;
hereby
assume
A1: R is
compatible;
let v,v9,w,w9 be
Element of M;
assume
A2: (
Class (R,v))
= (
Class (R,v9)) & (
Class (R,w))
= (
Class (R,w9));
per cases ;
suppose
A3: M is
empty;
hence (
Class (R,(v
* w)))
=
{}
.= (
Class (R,(v9
* w9))) by
A3;
end;
suppose not M is
empty;
then v
in (
Class (R,v9)) & w
in (
Class (R,w9)) by
A2,
EQREL_1: 23;
then (v
* w)
in (
Class (R,(v9
* w9))) by
A1;
hence (
Class (R,(v
* w)))
= (
Class (R,(v9
* w9))) by
EQREL_1: 23;
end;
end;
assume
A4: for v,v9,w,w9 be
Element of M st (
Class (R,v))
= (
Class (R,v9)) & (
Class (R,w))
= (
Class (R,w9)) holds (
Class (R,(v
* w)))
= (
Class (R,(v9
* w9)));
for v,v9,w,w9 be
Element of M st v
in (
Class (R,v9)) & w
in (
Class (R,w9)) holds (v
* w)
in (
Class (R,(v9
* w9)))
proof
let v,v9,w,w9 be
Element of M;
assume
A5: v
in (
Class (R,v9)) & w
in (
Class (R,w9));
per cases ;
suppose M is
empty;
hence thesis by
A5;
end;
suppose
A6: not M is
empty;
(
Class (R,v9))
= (
Class (R,v)) & (
Class (R,w9))
= (
Class (R,w)) by
A5,
EQREL_1: 23;
then (
Class (R,(v
* w)))
= (
Class (R,(v9
* w9))) by
A4;
hence (v
* w)
in (
Class (R,(v9
* w9))) by
A6,
EQREL_1: 23;
end;
end;
hence R is
compatible;
end;
definition
let M be
multMagma;
let R be
compatible
Equivalence_Relation of M;
::
ALGSTR_4:def4
func
ClassOp R ->
BinOp of (
Class R) means
:
Def4: for x,y be
Element of (
Class R), v,w be
Element of M st x
= (
Class (R,v)) & y
= (
Class (R,w)) holds (it
. (x,y))
= (
Class (R,(v
* w))) if M is non
empty
otherwise it
=
{} ;
correctness
proof
A1: not M is
empty implies ex b be
BinOp of (
Class R) st for x,y be
Element of (
Class R), v,w be
Element of M st x
= (
Class (R,v)) & y
= (
Class (R,w)) holds (b
. (x,y))
= (
Class (R,(v
* w)))
proof
assume
A2: not M is
empty;
then
reconsider X = (
Class R) as non
empty
set;
defpred
P[
set,
set,
set] means for x,y be
Element of (
Class R), v,w be
Element of M st x
= $1 & y
= $2 & x
= (
Class (R,v)) & y
= (
Class (R,w)) holds $3
= (
Class (R,(v
* w)));
A3: for x,y be
Element of X holds ex z be
Element of X st
P[x, y, z]
proof
let x,y be
Element of X;
x
in (
Class R);
then
consider v be
object such that
A4: v
in the
carrier of M & x
= (
Class (R,v)) by
EQREL_1:def 3;
reconsider v as
Element of M by
A4;
y
in (
Class R);
then
consider w be
object such that
A5: w
in the
carrier of M & y
= (
Class (R,w)) by
EQREL_1:def 3;
reconsider w as
Element of M by
A5;
reconsider z = (
Class (R,(v
* w))) as
Element of X by
A2,
EQREL_1:def 3;
take z;
thus thesis by
A4,
A5,
Th2;
end;
consider b be
Function of
[:X, X:], X such that
A6: for x,y be
Element of X holds
P[x, y, (b
. (x,y))] from
BINOP_1:sch 3(
A3);
reconsider b as
BinOp of (
Class R);
take b;
thus thesis by
A6;
end;
A7: M is
empty implies ex b be
BinOp of (
Class R) st b
=
{}
proof
assume M is
empty;
then the
carrier of M is
empty;
then
A8: (
Class R) is
empty;
set b = the
BinOp of (
Class R);
take b;
thus b
=
{} by
A8;
end;
for b1,b2 be
BinOp of (
Class R) holds not M is
empty & (for x,y be
Element of (
Class R), v,w be
Element of M st x
= (
Class (R,v)) & y
= (
Class (R,w)) holds (b1
. (x,y))
= (
Class (R,(v
* w)))) & (for x,y be
Element of (
Class R), v,w be
Element of M st x
= (
Class (R,v)) & y
= (
Class (R,w)) holds (b2
. (x,y))
= (
Class (R,(v
* w)))) implies b1
= b2
proof
let b1,b2 be
BinOp of (
Class R);
assume not M is
empty;
assume
A9: for x,y be
Element of (
Class R), v,w be
Element of M st x
= (
Class (R,v)) & y
= (
Class (R,w)) holds (b1
. (x,y))
= (
Class (R,(v
* w)));
assume
A10: for x,y be
Element of (
Class R), v,w be
Element of M st x
= (
Class (R,v)) & y
= (
Class (R,w)) holds (b2
. (x,y))
= (
Class (R,(v
* w)));
for x,y be
set st x
in (
Class R) & y
in (
Class R) holds (b1
. (x,y))
= (b2
. (x,y))
proof
let x,y be
set;
assume
A11: x
in (
Class R);
then
reconsider x9 = x as
Element of (
Class R);
assume
A12: y
in (
Class R);
then
reconsider y9 = y as
Element of (
Class R);
consider v be
object such that
A13: v
in the
carrier of M & x9
= (
Class (R,v)) by
A11,
EQREL_1:def 3;
consider w be
object such that
A14: w
in the
carrier of M & y9
= (
Class (R,w)) by
A12,
EQREL_1:def 3;
reconsider v, w as
Element of M by
A13,
A14;
(b1
. (x9,y9))
= (
Class (R,(v
* w))) by
A13,
A14,
A9;
hence (b1
. (x,y))
= (b2
. (x,y)) by
A13,
A14,
A10;
end;
hence thesis by
BINOP_1: 1;
end;
hence thesis by
A1,
A7;
end;
end
definition
let M be
multMagma;
let R be
compatible
Equivalence_Relation of M;
::
ALGSTR_4:def5
func M
./. R ->
multMagma equals
multMagma (# (
Class R), (
ClassOp R) #);
correctness ;
end
registration
let M be
multMagma;
let R be
compatible
Equivalence_Relation of M;
cluster (M
./. R) ->
strict;
correctness ;
end
registration
let M be non
empty
multMagma;
let R be
compatible
Equivalence_Relation of M;
cluster (M
./. R) -> non
empty;
correctness ;
end
definition
let M be non
empty
multMagma;
let R be
compatible
Equivalence_Relation of M;
::
ALGSTR_4:def6
func
nat_hom R ->
Function of M, (M
./. R) means
:
Def6: for v be
Element of M holds (it
. v)
= (
Class (R,v));
existence
proof
defpred
P[
object,
object] means ex v be
Element of M st $1
= v & $2
= (
Class (R,v));
A1: for x be
object st x
in the
carrier of M holds ex y be
object st
P[x, y]
proof
let x be
object;
assume x
in the
carrier of M;
then
reconsider v = x as
Element of M;
reconsider y = (
Class (R,v)) as
set;
take y, v;
thus thesis;
end;
consider f be
Function such that
A2: (
dom f)
= the
carrier of M and
A3: for x be
object st x
in the
carrier of M holds
P[x, (f
. x)] from
CLASSES1:sch 1(
A1);
(
rng f)
c= the
carrier of (M
./. R)
proof
let x be
object;
assume x
in (
rng f);
then
consider y be
object such that
A4: y
in (
dom f) and
A5: (f
. y)
= x by
FUNCT_1:def 3;
consider v be
Element of M such that
A6: y
= v & (f
. y)
= (
Class (R,v)) by
A2,
A3,
A4;
thus thesis by
A5,
A6,
EQREL_1:def 3;
end;
then
reconsider f as
Function of M, (M
./. R) by
A2,
FUNCT_2:def 1,
RELSET_1: 4;
take f;
let v be
Element of M;
ex w be
Element of M st v
= w & (f
. v)
= (
Class (R,w)) by
A3;
hence thesis;
end;
uniqueness
proof
let f1,f2 be
Function of M, (M
./. R) such that
A7: for v be
Element of M holds (f1
. v)
= (
Class (R,v)) and
A8: for v be
Element of M holds (f2
. v)
= (
Class (R,v));
now
let v be
Element of M;
(f1
. v)
= (
Class (R,v)) & (f2
. v)
= (
Class (R,v)) by
A7,
A8;
hence (f1
. v)
= (f2
. v);
end;
hence thesis by
FUNCT_2: 63;
end;
end
registration
let M be non
empty
multMagma;
let R be
compatible
Equivalence_Relation of M;
cluster (
nat_hom R) ->
multiplicative;
correctness
proof
for v,w be
Element of M holds ((
nat_hom R)
. (v
* w))
= (((
nat_hom R)
. v)
* ((
nat_hom R)
. w))
proof
let v,w be
Element of M;
((
nat_hom R)
. v)
= (
Class (R,v)) & ((
nat_hom R)
. w)
= (
Class (R,w)) by
Def6;
then ((
ClassOp R)
. (((
nat_hom R)
. v),((
nat_hom R)
. w)))
= (
Class (R,(v
* w))) by
Def4;
hence ((
nat_hom R)
. (v
* w))
= (((
nat_hom R)
. v)
* ((
nat_hom R)
. w)) by
Def6;
end;
hence thesis by
GROUP_6:def 6;
end;
end
registration
let M be non
empty
multMagma;
let R be
compatible
Equivalence_Relation of M;
cluster (
nat_hom R) ->
onto;
correctness
proof
for y be
object st y
in the
carrier of (M
./. R) holds y
in (
rng (
nat_hom R))
proof
let y be
object;
assume y
in the
carrier of (M
./. R);
then
consider x be
object such that
A1: x
in the
carrier of M & y
= (
Class (R,x)) by
EQREL_1:def 3;
reconsider x as
Element of M by
A1;
the
carrier of M
= (
dom (
nat_hom R)) by
FUNCT_2:def 1;
then x
in (
dom (
nat_hom R)) & ((
nat_hom R)
. x)
= (
Class (R,x)) by
Def6;
hence y
in (
rng (
nat_hom R)) by
A1,
FUNCT_1:def 3;
end;
then the
carrier of (M
./. R)
c= (
rng (
nat_hom R));
then (
rng (
nat_hom R))
= the
carrier of (M
./. R) by
XBOOLE_0:def 10;
hence thesis by
FUNCT_2:def 3;
end;
end
definition
let M be
multMagma;
mode
Relators of M is
[:the
carrier of M, the
carrier of M:]
-valued
Function;
end
definition
let M be
multMagma;
let r be
Relators of M;
::
ALGSTR_4:def7
func
equ_rel r ->
Equivalence_Relation of M equals (
meet { R where R be
compatible
Equivalence_Relation of M : for i be
set, v,w be
Element of M st i
in (
dom r) & (r
. i)
=
[v, w] holds v
in (
Class (R,w)) });
correctness
proof
set X = { R where R be
compatible
Equivalence_Relation of M : for i be
set, v,w be
Element of M st i
in (
dom r) & (r
. i)
=
[v, w] holds v
in (
Class (R,w)) };
per cases ;
suppose M is
empty;
then
A1: the
carrier of M
=
{} ;
for x be
object st x
in X holds x
in
{
{} }
proof
let x be
object;
assume x
in X;
then
consider R be
compatible
Equivalence_Relation of M such that
A2: x
= R & for i be
set, v,w be
Element of M st i
in (
dom r) & (r
. i)
=
[v, w] holds v
in (
Class (R,w));
x is
Subset of
{} by
A2,
A1,
ZFMISC_1: 90;
hence x
in
{
{} } by
TARSKI:def 1;
end;
then X
c=
{
{} };
then X
=
{} or X
=
{
{} } by
ZFMISC_1: 33;
hence thesis by
A1,
OSALG_4: 9,
SETFAM_1: 10,
SETFAM_1:def 1;
end;
suppose
A3: not M is
empty;
for i be
set, v,w be
Element of M st i
in (
dom r) & (r
. i)
=
[v, w] holds v
in (
Class ((
nabla the
carrier of M),w))
proof
let i be
set;
let v,w be
Element of M;
assume i
in (
dom r) & (r
. i)
=
[v, w];
(
Class ((
nabla the
carrier of M),w))
= the
carrier of M by
A3,
EQREL_1: 26;
hence v
in (
Class ((
nabla the
carrier of M),w)) by
A3,
SUBSET_1:def 1;
end;
then
A4: (
nabla the
carrier of M)
in X;
for x be
object st x
in X holds x
in (
bool
[:the
carrier of M, the
carrier of M:])
proof
let x be
object;
assume x
in X;
then
consider R be
compatible
Equivalence_Relation of M such that
A5: x
= R & for i be
set, x,y be
Element of M st i
in (
dom r) & (r
. i)
=
[x, y] holds x
in (
Class (R,y));
thus thesis by
A5;
end;
then
reconsider X as
Subset-Family of
[:the
carrier of M, the
carrier of M:] by
TARSKI:def 3;
for Y be
set st Y
in X holds Y is
Equivalence_Relation of M
proof
let Y be
set;
assume Y
in X;
then
consider R be
compatible
Equivalence_Relation of M such that
A6: Y
= R & for i be
set, v,w be
Element of M st i
in (
dom r) & (r
. i)
=
[v, w] holds v
in (
Class (R,w));
thus Y is
Equivalence_Relation of M by
A6;
end;
hence thesis by
A4,
EQREL_1: 11;
end;
end;
end
theorem ::
ALGSTR_4:3
Th3: for M be
multMagma, r be
Relators of M, R be
compatible
Equivalence_Relation of M st (for i be
set, v,w be
Element of M st i
in (
dom r) & (r
. i)
=
[v, w] holds v
in (
Class (R,w))) holds (
equ_rel r)
c= R
proof
let M be
multMagma;
let r be
Relators of M;
let R be
compatible
Equivalence_Relation of M;
assume
A1: for i be
set, v,w be
Element of M st i
in (
dom r) & (r
. i)
=
[v, w] holds v
in (
Class (R,w));
let X be
object;
R
in { R9 where R9 be
compatible
Equivalence_Relation of M : for i be
set, v,w be
Element of M st i
in (
dom r) & (r
. i)
=
[v, w] holds v
in (
Class (R9,w)) } by
A1;
hence thesis by
SETFAM_1:def 1;
end;
registration
let M be
multMagma;
let r be
Relators of M;
cluster (
equ_rel r) ->
compatible;
coherence
proof
set X = { R where R be
compatible
Equivalence_Relation of M : for i be
set, v,w be
Element of M st i
in (
dom r) & (r
. i)
=
[v, w] holds v
in (
Class (R,w)) };
for v,v9,w,w9 be
Element of M st v
in (
Class ((
equ_rel r),v9)) & w
in (
Class ((
equ_rel r),w9)) holds (v
* w)
in (
Class ((
equ_rel r),(v9
* w9)))
proof
let v,v9,w,w9 be
Element of M;
assume v
in (
Class ((
equ_rel r),v9));
then
A1:
[v9, v]
in (
equ_rel r) by
EQREL_1: 18;
assume w
in (
Class ((
equ_rel r),w9));
then
A2:
[w9, w]
in (
equ_rel r) by
EQREL_1: 18;
per cases ;
suppose X
=
{} ;
hence thesis by
A1,
SETFAM_1:def 1;
end;
suppose
A3: X
<>
{} ;
for Y be
set st Y
in X holds
[(v9
* w9), (v
* w)]
in Y
proof
let Y be
set;
assume
A4: Y
in X;
then
consider R be
compatible
Equivalence_Relation of M such that
A5: Y
= R & for i be
set, v,w be
Element of M st i
in (
dom r) & (r
. i)
=
[v, w] holds v
in (
Class (R,w));
[v9, v]
in Y by
A1,
A4,
SETFAM_1:def 1;
then
A6: v
in (
Class (R,v9)) by
A5,
EQREL_1: 18;
[w9, w]
in Y by
A2,
A4,
SETFAM_1:def 1;
then w
in (
Class (R,w9)) by
A5,
EQREL_1: 18;
then (v
* w)
in (
Class (R,(v9
* w9))) by
A6,
Def3;
hence
[(v9
* w9), (v
* w)]
in Y by
A5,
EQREL_1: 18;
end;
then
[(v9
* w9), (v
* w)]
in (
meet X) by
A3,
SETFAM_1:def 1;
hence (v
* w)
in (
Class ((
equ_rel r),(v9
* w9))) by
EQREL_1: 18;
end;
end;
hence thesis;
end;
end
definition
let X,Y be
set;
let f be
Function of X, Y;
::
ALGSTR_4:def8
func
equ_kernel f ->
Equivalence_Relation of X means
:
Def8: for x,y be
object holds
[x, y]
in it iff x
in X & y
in X & (f
. x)
= (f
. y);
existence
proof
defpred
P[
object,
object] means (f
. $1)
= (f
. $2);
A1: for x be
object st x
in X holds
P[x, x];
A2: for x,y be
object st
P[x, y] holds
P[y, x];
A3: for x,y,z be
object st
P[x, y] &
P[y, z] holds
P[x, z];
ex EqR be
Equivalence_Relation of X st for x,y be
object holds
[x, y]
in EqR iff x
in X & y
in X &
P[x, y] from
EQREL_1:sch 1(
A1,
A2,
A3);
hence thesis;
end;
uniqueness
proof
let R1,R2 be
Equivalence_Relation of X;
defpred
P[
object,
object] means $1
in X & $2
in X & (f
. $1)
= (f
. $2);
assume for x,y be
object holds
[x, y]
in R1 iff x
in X & y
in X & (f
. x)
= (f
. y);
then
A4: for x,y be
object holds
[x, y]
in R1 iff
P[x, y];
assume for x,y be
object holds
[x, y]
in R2 iff x
in X & y
in X & (f
. x)
= (f
. y);
then
A5: for x,y be
object holds
[x, y]
in R2 iff
P[x, y];
thus R1
= R2 from
RELAT_1:sch 2(
A4,
A5);
end;
end
reserve M,N for non
empty
multMagma,
f for
Function of M, N;
theorem ::
ALGSTR_4:4
Th4: f is
multiplicative implies (
equ_kernel f) is
compatible
proof
assume
A1: f is
multiplicative;
set R = (
equ_kernel f);
for v,v9,w,w9 be
Element of M st v
in (
Class (R,v9)) & w
in (
Class (R,w9)) holds (v
* w)
in (
Class (R,(v9
* w9)))
proof
let v,v9,w,w9 be
Element of M;
assume v
in (
Class (R,v9));
then
A2:
[v9, v]
in R by
EQREL_1: 18;
assume w
in (
Class (R,w9));
then
[w9, w]
in R by
EQREL_1: 18;
then
A3: (f
. w9)
= (f
. w) by
Def8;
(f
. (v9
* w9))
= ((f
. v9)
* (f
. w9)) by
A1,
GROUP_6:def 6
.= ((f
. v)
* (f
. w)) by
A2,
A3,
Def8
.= (f
. (v
* w)) by
A1,
GROUP_6:def 6;
then
[(v9
* w9), (v
* w)]
in R by
Def8;
hence (v
* w)
in (
Class (R,(v9
* w9))) by
EQREL_1: 18;
end;
hence (
equ_kernel f) is
compatible;
end;
theorem ::
ALGSTR_4:5
Th5: f is
multiplicative implies ex r be
Relators of M st (
equ_kernel f)
= (
equ_rel r)
proof
assume
A1: f is
multiplicative;
set I = {
[v, w] where v,w be
Element of M : (f
. v)
= (f
. w) };
set r = (
id I);
for y be
object st y
in (
rng r) holds y
in
[:the
carrier of M, the
carrier of M:]
proof
let y be
object;
assume y
in (
rng r);
then
consider x be
object such that
A2: x
in (
dom r) & y
= (r
. x) by
FUNCT_1:def 3;
y
= x by
A2,
FUNCT_1: 17;
then y
in I by
A2;
then
consider v9,w9 be
Element of M such that
A3: y
=
[v9, w9] & (f
. v9)
= (f
. w9);
thus thesis by
A3,
ZFMISC_1:def 2;
end;
then (
rng r)
c=
[:the
carrier of M, the
carrier of M:];
then
reconsider r as
Relators of M by
FUNCT_2: 2;
take r;
reconsider R = (
equ_kernel f) as
compatible
Equivalence_Relation of M by
A1,
Th4;
A4: for i be
set, v,w be
Element of M st i
in (
dom r) & (r
. i)
=
[v, w] holds v
in (
Class (R,w))
proof
let i be
set;
let v,w be
Element of M;
assume
A5: i
in (
dom r) & (r
. i)
=
[v, w];
then
A6: (r
. i)
= i by
FUNCT_1: 17;
consider v9,w9 be
Element of M such that
A7: i
=
[v9, w9] & (f
. v9)
= (f
. w9) by
A5;
[v, w]
in (
equ_kernel f) by
A7,
Def8,
A5,
A6;
hence v
in (
Class (R,w)) by
EQREL_1: 19;
end;
then
A8: (
equ_rel r)
c= R by
Th3;
for z be
object st z
in R holds z
in (
equ_rel r)
proof
let z be
object;
assume
A9: z
in R;
then
consider x,y be
object such that
A10: x
in the
carrier of M & y
in the
carrier of M & z
=
[x, y] by
ZFMISC_1:def 2;
A11: (f
. x)
= (f
. y) by
A9,
A10,
Def8;
reconsider x, y as
Element of M by
A10;
set X9 = { R9 where R9 be
compatible
Equivalence_Relation of M : for i be
set, v,w be
Element of M st i
in (
dom r) & (r
. i)
=
[v, w] holds v
in (
Class (R9,w)) };
A12: R
in X9 by
A4;
for Y be
set st Y
in X9 holds z
in Y
proof
let Y be
set;
assume Y
in X9;
then
consider R9 be
compatible
Equivalence_Relation of M such that
A13: R9
= Y & for i be
set, v,w be
Element of M st i
in (
dom r) & (r
. i)
=
[v, w] holds v
in (
Class (R9,w));
set i =
[x, y];
A14: i
in I by
A11;
then (r
. i)
=
[x, y] by
FUNCT_1: 17;
then x
in (
Class (R9,y)) by
A14,
A13;
hence z
in Y by
A10,
A13,
EQREL_1: 19;
end;
hence thesis by
A12,
SETFAM_1:def 1;
end;
then R
c= (
equ_rel r);
hence thesis by
A8,
XBOOLE_0:def 10;
end;
begin
definition
let M be
multMagma;
::
ALGSTR_4:def9
mode
multSubmagma of M ->
multMagma means
:
Def9: the
carrier of it
c= the
carrier of M & the
multF of it
= (the
multF of M
|| the
carrier of it );
existence
proof
set S = the
empty
multMagma;
reconsider A = the
carrier of S as
set;
reconsider X =
[:A, A:] as
set;
the
multF of S
= (the
multF of M
|
{} )
.= (the
multF of M
| X) by
ZFMISC_1: 90
.= (the
multF of M
|| the
carrier of S) by
REALSET1:def 2;
hence thesis by
XBOOLE_1: 2;
end;
end
registration
let M be
multMagma;
cluster
strict for
multSubmagma of M;
existence
proof
set N =
multMagma (# the
carrier of M, the
multF of M #);
the
multF of N
= (the
multF of N
|
[:the
carrier of N, the
carrier of N:])
.= (the
multF of M
|| the
carrier of N) by
REALSET1:def 2;
then
reconsider N as
multSubmagma of M by
Def9;
take N;
thus thesis;
end;
end
registration
let M be non
empty
multMagma;
cluster non
empty for
multSubmagma of M;
existence
proof
set N =
multMagma (# the
carrier of M, the
multF of M #);
the
multF of N
= (the
multF of N
|
[:the
carrier of N, the
carrier of N:])
.= (the
multF of M
|| the
carrier of N) by
REALSET1:def 2;
then
reconsider N as
multSubmagma of M by
Def9;
take N;
thus thesis;
end;
end
reserve M for
multMagma;
reserve N,K for
multSubmagma of M;
theorem ::
ALGSTR_4:6
Th6: N is
multSubmagma of K & K is
multSubmagma of N implies the multMagma of N
= the multMagma of K
proof
assume that
A1: N is
multSubmagma of K and
A2: K is
multSubmagma of N;
set A = the
carrier of N;
set B = the
carrier of K;
set f = the
multF of N;
set g = the
multF of K;
A3: A
c= B & B
c= A by
A1,
A2,
Def9;
f
= (g
|| A) by
A1,
Def9
.= ((f
|| B)
|| A) by
A2,
Def9
.= ((f
|
[:B, B:])
|| A) by
REALSET1:def 2
.= ((f
|
[:B, B:])
|
[:A, A:]) by
REALSET1:def 2
.= (f
|
[:B, B:])
.= (f
|| B) by
REALSET1:def 2
.= g by
A2,
Def9;
hence thesis by
A3,
XBOOLE_0:def 10;
end;
theorem ::
ALGSTR_4:7
Th7: the
carrier of N
= the
carrier of M implies the multMagma of N
= the multMagma of M
proof
assume
A1: the
carrier of N
= the
carrier of M;
per cases ;
suppose the
carrier of M
=
{} ;
hence thesis by
A1;
end;
suppose the
carrier of M
<>
{} ;
A2: the
multF of M
= (the
multF of M
|
[:the
carrier of M, the
carrier of M:])
.= (the
multF of M
|| the
carrier of M) by
REALSET1:def 2;
then
reconsider M9 = M as
multSubmagma of M by
Def9;
the
multF of M9
= (the
multF of N
|| the
carrier of M9) by
A1,
A2,
Def9;
then M9 is
multSubmagma of N by
A1,
Def9;
hence thesis by
Th6;
end;
end;
definition
let M be
multMagma;
let A be
Subset of M;
::
ALGSTR_4:def10
attr A is
stable means
:
Def10: for v,w be
Element of M st v
in A & w
in A holds (v
* w)
in A;
end
registration
let M be
multMagma;
cluster
stable for
Subset of M;
correctness
proof
reconsider A = the
carrier of M as
Subset of M by
ZFMISC_1:def 1;
take A;
thus thesis;
end;
end
theorem ::
ALGSTR_4:8
Th8: the
carrier of N is
stable
Subset of M
proof
for v,w be
Element of M st v
in the
carrier of N & w
in the
carrier of N holds (v
* w)
in the
carrier of N
proof
let v,w be
Element of M;
assume
A1: v
in the
carrier of N & w
in the
carrier of N;
then
reconsider v9 = v, w9 = w as
Element of N;
A2:
[v, w]
in
[:the
carrier of N, the
carrier of N:] by
A1,
ZFMISC_1:def 2;
(v9
* w9)
= (the
multF of N
.
[v9, w9]) by
BINOP_1:def 1
.= ((the
multF of M
|| the
carrier of N)
.
[v9, w9]) by
Def9
.= ((the
multF of M
|
[:the
carrier of N, the
carrier of N:])
.
[v, w]) by
REALSET1:def 2
.= (the
multF of M
.
[v, w]) by
A2,
FUNCT_1: 49
.= (v
* w) by
BINOP_1:def 1;
hence (v
* w)
in the
carrier of N by
A1;
end;
hence the
carrier of N is
stable
Subset of M by
Def9,
Def10;
end;
registration
let M be
multMagma;
let N be
multSubmagma of M;
cluster the
carrier of N ->
stable;
correctness by
Th8;
end
theorem ::
ALGSTR_4:9
Th9: for F be
Function st (for i be
set st i
in (
dom F) holds (F
. i) is
stable
Subset of M) holds (
meet F) is
stable
Subset of M
proof
let F be
Function;
assume
A1: for i be
set st i
in (
dom F) holds (F
. i) is
stable
Subset of M;
A2: for x be
object st x
in (
meet F) holds x
in the
carrier of M
proof
let x be
object;
assume x
in (
meet F);
then
A3: x
in (
meet (
rng F)) by
FUNCT_6:def 4;
per cases ;
suppose (
dom F) is
empty;
then F
=
{} ;
hence thesis by
A3,
SETFAM_1: 1;
end;
suppose not (
dom F) is
empty;
then
consider i be
object such that
A4: i
in (
dom F) by
XBOOLE_0:def 1;
(
meet (
rng F))
c= (F
. i) by
A4,
FUNCT_1: 3,
SETFAM_1: 3;
then
A5: x
in (F
. i) by
A3;
(F
. i) is
stable
Subset of M by
A1,
A4;
hence x
in the
carrier of M by
A5;
end;
end;
for v,w be
Element of M st v
in (
meet F) & w
in (
meet F) holds (v
* w)
in (
meet F)
proof
let v,w be
Element of M;
assume
A6: v
in (
meet F) & w
in (
meet F);
per cases ;
suppose F
=
{} ;
then (
meet (
rng F))
=
{} by
SETFAM_1: 1;
hence thesis by
A6,
FUNCT_6:def 4;
end;
suppose
A7: F
<>
{} ;
A8: v
in (
meet (
rng F)) & w
in (
meet (
rng F)) by
A6,
FUNCT_6:def 4;
for Y be
set holds Y
in (
rng F) implies (v
* w)
in Y
proof
let Y be
set;
assume
A9: Y
in (
rng F);
then
A10: v
in Y & w
in Y by
A8,
SETFAM_1:def 1;
consider i be
object such that
A11: i
in (
dom F) & Y
= (F
. i) by
A9,
FUNCT_1:def 3;
Y is
stable
Subset of M by
A1,
A11;
hence (v
* w)
in Y by
A10,
Def10;
end;
then (v
* w)
in (
meet (
rng F)) by
A7,
SETFAM_1:def 1;
hence (v
* w)
in (
meet F) by
FUNCT_6:def 4;
end;
end;
hence thesis by
A2,
Def10,
TARSKI:def 3;
end;
reserve M,N for non
empty
multMagma,
A for
Subset of M,
f,g for
Function of M, N,
X for
stable
Subset of M,
Y for
stable
Subset of N;
theorem ::
ALGSTR_4:10
A is
stable iff (A
* A)
c= A
proof
hereby
assume
A1: A is
stable;
for x be
object st x
in (A
* A) holds x
in A
proof
let x be
object;
assume x
in (A
* A);
then
consider v,w be
Element of M such that
A2: x
= (v
* w) & v
in A & w
in A by
GROUP_2: 8;
thus x
in A by
A1,
A2;
end;
hence (A
* A)
c= A;
end;
assume
A3: (A
* A)
c= A;
for v,w be
Element of M st v
in A & w
in A holds (v
* w)
in A
proof
let v,w be
Element of M;
assume v
in A & w
in A;
then (v
* w)
in (A
* A) by
GROUP_2: 8;
hence (v
* w)
in A by
A3;
end;
hence A is
stable;
end;
theorem ::
ALGSTR_4:11
Th11: f is
multiplicative implies (f
.: X) is
stable
Subset of N
proof
assume
A1: f is
multiplicative;
for v,w be
Element of N st v
in (f
.: X) & w
in (f
.: X) holds (v
* w)
in (f
.: X)
proof
let v,w be
Element of N;
assume v
in (f
.: X);
then
consider v9 be
object such that
A2: v9
in (
dom f) & v9
in X & v
= (f
. v9) by
FUNCT_1:def 6;
assume w
in (f
.: X);
then
consider w9 be
object such that
A3: w9
in (
dom f) & w9
in X & w
= (f
. w9) by
FUNCT_1:def 6;
reconsider v9, w9 as
Element of M by
A2,
A3;
(v9
* w9)
in the
carrier of M;
then
A4: (v9
* w9)
in (
dom f) by
FUNCT_2:def 1;
(v9
* w9)
in X by
A2,
A3,
Def10;
then (f
. (v9
* w9))
in (f
.: X) by
A4,
FUNCT_1:def 6;
hence (v
* w)
in (f
.: X) by
A2,
A3,
A1,
GROUP_6:def 6;
end;
hence (f
.: X) is
stable
Subset of N by
Def10;
end;
theorem ::
ALGSTR_4:12
Th12: f is
multiplicative implies (f
" Y) is
stable
Subset of M
proof
assume
A1: f is
multiplicative;
for v,w be
Element of M st v
in (f
" Y) & w
in (f
" Y) holds (v
* w)
in (f
" Y)
proof
let v,w be
Element of M;
assume v
in (f
" Y);
then
A2: v
in (
dom f) & (f
. v)
in Y by
FUNCT_1:def 7;
assume w
in (f
" Y);
then
A3: w
in (
dom f) & (f
. w)
in Y by
FUNCT_1:def 7;
(v
* w)
in the
carrier of M;
then
A4: (v
* w)
in (
dom f) by
FUNCT_2:def 1;
((f
. v)
* (f
. w))
in Y by
A2,
A3,
Def10;
then (f
. (v
* w))
in Y by
A1,
GROUP_6:def 6;
hence (v
* w)
in (f
" Y) by
A4,
FUNCT_1:def 7;
end;
hence (f
" Y) is
stable
Subset of M by
Def10;
end;
theorem ::
ALGSTR_4:13
f is
multiplicative & g is
multiplicative implies { v where v be
Element of M : (f
. v)
= (g
. v) } is
stable
Subset of M
proof
assume
A1: f is
multiplicative;
assume
A2: g is
multiplicative;
set X = { v where v be
Element of M : (f
. v)
= (g
. v) };
for x be
object st x
in X holds x
in the
carrier of M
proof
let x be
object;
assume x
in X;
then
consider v be
Element of M such that
A3: x
= v & (f
. v)
= (g
. v);
thus x
in the
carrier of M by
A3;
end;
then
reconsider X as
Subset of M by
TARSKI:def 3;
for v,w be
Element of M st v
in X & w
in X holds (v
* w)
in X
proof
let v,w be
Element of M;
assume v
in X;
then
consider v9 be
Element of M such that
A4: v
= v9 & (f
. v9)
= (g
. v9);
assume w
in X;
then
consider w9 be
Element of M such that
A5: w
= w9 & (f
. w9)
= (g
. w9);
(f
. (v
* w))
= ((g
. v)
* (g
. w)) by
A4,
A5,
A1,
GROUP_6:def 6
.= (g
. (v
* w)) by
A2,
GROUP_6:def 6;
hence (v
* w)
in X;
end;
hence thesis by
Def10;
end;
definition
let M be
multMagma;
let A be
stable
Subset of M;
::
ALGSTR_4:def11
func
the_mult_induced_by A ->
BinOp of A equals (the
multF of M
|| A);
correctness
proof
for x be
set holds x
in
[:A, A:] implies (the
multF of M
. x)
in A
proof
let x be
set;
assume x
in
[:A, A:];
then
consider v,w be
object such that
A1: v
in A & w
in A & x
=
[v, w] by
ZFMISC_1:def 2;
reconsider v, w as
Element of M by
A1;
(v
* w)
in A by
A1,
Def10;
hence (the
multF of M
. x)
in A by
A1,
BINOP_1:def 1;
end;
then A is
Preserv of the
multF of M by
REALSET1:def 1;
hence thesis by
REALSET1: 2;
end;
end
definition
let M be
multMagma;
let A be
Subset of M;
::
ALGSTR_4:def12
func
the_submagma_generated_by A ->
strict
multSubmagma of M means
:
Def12: A
c= the
carrier of it & for N be
strict
multSubmagma of M st A
c= the
carrier of N holds it is
multSubmagma of N;
existence
proof
defpred
P[
set] means ex H be
strict
multSubmagma of M st $1
= the
carrier of H & A
c= $1;
consider X be
set such that
A1: for Y be
set holds Y
in X iff Y
in (
bool the
carrier of M) &
P[Y] from
XFAMILY:sch 1;
set F = (
id X);
set A1 = (
meet (
id X));
for x be
set st x
in (
dom F) holds (F
. x) is
stable
Subset of M
proof
let x be
set;
assume
A2: x
in (
dom F);
then x
in (
bool the
carrier of M) &
P[x] by
A1;
hence thesis by
A2,
FUNCT_1: 18;
end;
then
reconsider A1 as
stable
Subset of M by
Th9;
set N1 =
multMagma (# A1, (
the_mult_induced_by A1) #);
take N1;
per cases ;
suppose
A3: X
=
{} ;
A4: the
carrier of M
in (
bool the
carrier of M) by
ZFMISC_1:def 1;
ex H be
strict
multSubmagma of M st the
carrier of M
= the
carrier of H & A
c= the
carrier of M
proof
the
multF of M
= (the
multF of M
|
[:the
carrier of M, the
carrier of M:]);
then the
multF of M
= (the
multF of M
|| the
carrier of M) by
REALSET1:def 2;
then
reconsider H = the multMagma of M as
strict
multSubmagma of M by
Def9;
take H;
thus the
carrier of M
= the
carrier of H;
thus A
c= the
carrier of M;
end;
hence thesis by
A3,
A4,
A1;
end;
suppose
A5: X
<>
{} ;
A6: for x be
object st x
in A holds x
in A1
proof
let x be
object;
assume
A7: x
in A;
for Y be
set st Y
in X holds x
in Y
proof
let Y be
set;
assume Y
in X;
then
consider H be
strict
multSubmagma of M such that
A8: Y
= the
carrier of H & A
c= Y by
A1;
thus x
in Y by
A8,
A7;
end;
then x
in (
meet X) by
A5,
SETFAM_1:def 1;
then x
in (
meet (
rng (
id X)));
hence thesis by
FUNCT_6:def 4;
end;
for N be
strict
multSubmagma of M st A
c= the
carrier of N holds N1 is
multSubmagma of N
proof
let N be
strict
multSubmagma of M;
assume
A9: A
c= the
carrier of N;
for x be
object st x
in the
carrier of N1 holds x
in the
carrier of N
proof
let x be
object;
assume x
in the
carrier of N1;
then x
in (
meet (
rng (
id X))) by
FUNCT_6:def 4;
then
A10: x
in (
meet X);
the
carrier of N
c= the
carrier of M by
Def9;
then the
carrier of N
in X by
A1,
A9;
hence x
in the
carrier of N by
A10,
SETFAM_1:def 1;
end;
then
A11: the
carrier of N1
c= the
carrier of N;
A12: (the
multF of M
|
[:the
carrier of N, the
carrier of N:])
= (the
multF of M
|| the
carrier of N) by
REALSET1:def 2
.= the
multF of N by
Def9;
the
multF of N1
= (the
multF of M
|
[:the
carrier of N1, the
carrier of N1:]) by
REALSET1:def 2
.= ((the
multF of M
|
[:the
carrier of N, the
carrier of N:])
|
[:the
carrier of N1, the
carrier of N1:]) by
A11,
RELAT_1: 74,
ZFMISC_1: 96
.= (the
multF of N
|| the
carrier of N1) by
A12,
REALSET1:def 2;
hence N1 is
multSubmagma of N by
A11,
Def9;
end;
hence thesis by
A6,
Def9;
end;
end;
uniqueness
proof
let H1,H2 be
strict
multSubmagma of M;
assume A
c= the
carrier of H1 & (for N be
strict
multSubmagma of M st A
c= the
carrier of N holds H1 is
multSubmagma of N) & A
c= the
carrier of H2 & (for N be
strict
multSubmagma of M st A
c= the
carrier of N holds H2 is
multSubmagma of N);
then H1 is
multSubmagma of H2 & H2 is
multSubmagma of H1;
hence thesis by
Th6;
end;
end
theorem ::
ALGSTR_4:14
Th14: for M be
multMagma, A be
Subset of M holds A is
empty iff (
the_submagma_generated_by A) is
empty
proof
let M be
multMagma;
let A be
Subset of M;
hereby
assume
A1: A is
empty;
then for v,w be
Element of M st v
in A & w
in A holds (v
* w)
in A;
then
reconsider A9 = A as
stable
Subset of M by
Def10;
reconsider N =
multMagma (# A9, (
the_mult_induced_by A9) #) as
strict
multSubmagma of M by
Def9;
(
the_submagma_generated_by A) is
multSubmagma of N by
Def12;
then the
carrier of (
the_submagma_generated_by A)
c= the
carrier of N by
Def9;
hence (
the_submagma_generated_by A) is
empty by
A1;
end;
assume (
the_submagma_generated_by A) is
empty;
then the
carrier of (
the_submagma_generated_by A)
=
{} ;
then A
c=
{} by
Def12;
hence A is
empty;
end;
registration
let M be
multMagma;
let A be
empty
Subset of M;
cluster (
the_submagma_generated_by A) ->
empty;
correctness by
Th14;
end
theorem ::
ALGSTR_4:15
Th15: for M,N be non
empty
multMagma, f be
Function of M, N, X be
Subset of M st f is
multiplicative holds (f
.: the
carrier of (
the_submagma_generated_by X))
= the
carrier of (
the_submagma_generated_by (f
.: X))
proof
let M,N be non
empty
multMagma;
let f be
Function of M, N;
let X be
Subset of M;
assume
A1: f is
multiplicative;
set X9 = (
the_submagma_generated_by X);
set A = (f
.: the
carrier of X9);
the
carrier of X9 is
stable
Subset of M by
Th8;
then
reconsider A as
stable
Subset of N by
A1,
Th11;
set Y9 = (
the_submagma_generated_by (f
.: X));
set B = (f
" the
carrier of Y9);
the
carrier of Y9 is
stable
Subset of N by
Th8;
then
reconsider B as
stable
Subset of M by
A1,
Th12;
A2: (f
.: X)
c= the
carrier of Y9 & for N1 be
strict
multSubmagma of N st (f
.: X)
c= the
carrier of N1 holds Y9 is
multSubmagma of N1 by
Def12;
reconsider N1 =
multMagma (# A, (
the_mult_induced_by A) #) as
strict
multSubmagma of N by
Def9;
X
c= the
carrier of X9 by
Def12;
then Y9 is
multSubmagma of N1 by
A2,
RELAT_1: 123;
then
A3: the
carrier of Y9
c= A by
Def9;
A4: X
c= the
carrier of X9 & for M1 be
strict
multSubmagma of M st X
c= the
carrier of M1 holds X9 is
multSubmagma of M1 by
Def12;
reconsider M1 =
multMagma (# B, (
the_mult_induced_by B) #) as
strict
multSubmagma of M by
Def9;
A5: (f
.: (f
" the
carrier of Y9))
c= the
carrier of Y9 by
FUNCT_1: 75;
(f
.: X)
c= the
carrier of (
the_submagma_generated_by (f
.: X)) by
Def12;
then
A6: (f
" (f
.: X))
c= (f
" the
carrier of (
the_submagma_generated_by (f
.: X))) by
RELAT_1: 143;
X
c= the
carrier of M;
then X
c= (
dom f) by
FUNCT_2:def 1;
then X
c= (f
" (f
.: X)) by
FUNCT_1: 76;
then X9 is
multSubmagma of M1 by
A4,
A6,
XBOOLE_1: 1;
then the
carrier of X9
c= B by
Def9;
then A
c= (f
.: (f
" the
carrier of Y9)) by
RELAT_1: 123;
then A
c= the
carrier of Y9 by
A5;
hence thesis by
A3,
XBOOLE_0:def 10;
end;
begin
definition
let X be
set;
defpred
P[
object,
object] means for fs be
XFinSequence of (
bool (
the_universe_of (X
\/
NAT ))) st $1
= fs holds ((
dom fs)
=
0 implies $2
=
{} ) & ((
dom fs)
= 1 implies $2
= X) & for n be
Nat st n
>= 2 & (
dom fs)
= n holds ex fs1 be
FinSequence st (
len fs1)
= (n
- 1) & (for p be
Nat st p
>= 1 & p
<= (n
- 1) holds (fs1
. p)
=
[:(fs
. p), (fs
. (n
- p)):]) & $2
= (
Union (
disjoin fs1));
A1: for e be
object st e
in ((
bool (
the_universe_of (X
\/
NAT )))
^omega ) holds ex u be
object st
P[e, u]
proof
let e be
object;
assume e
in ((
bool (
the_universe_of (X
\/
NAT )))
^omega );
then
reconsider fs = e as
XFinSequence of (
bool (
the_universe_of (X
\/
NAT ))) by
AFINSQ_1:def 7;
(
dom fs)
=
0 or ((
dom fs)
+ 1)
> (
0
+ 1) by
XREAL_1: 6;
then (
dom fs)
=
0 or (
dom fs)
>= 1 by
NAT_1: 13;
then (
dom fs)
=
0 or (
dom fs)
= 1 or (
dom fs)
> 1 by
XXREAL_0: 1;
then
A2: (
dom fs)
=
0 or (
dom fs)
= 1 or ((
dom fs)
+ 1)
> (1
+ 1) by
XREAL_1: 6;
per cases by
A2,
NAT_1: 13;
suppose
A3: (
dom fs)
=
0 ;
set u =
{} ;
take u;
thus
P[e, u] by
A3;
end;
suppose
A4: (
dom fs)
= 1;
set u = X;
take u;
thus
P[e, u] by
A4;
end;
suppose
A5: (
dom fs)
>= 2;
reconsider n = (
dom fs) as
Nat;
reconsider n9 = (n
-' 1) as
Nat;
(n
- 1)
>= (2
- 1) by
A5,
XREAL_1: 9;
then
A6: n9
= (n
- 1) by
XREAL_0:def 2;
defpred
P2[
set,
object] means for p be
Nat st p
>= 1 & p
<= (n
- 1) & $1
= p holds $2
=
[:(fs
. p), (fs
. (n
- p)):];
A7: for k be
Nat st k
in (
Seg n9) holds ex x be
object st
P2[k, x]
proof
let k be
Nat;
assume k
in (
Seg n9);
set x =
[:(fs
. k), (fs
. (n
- k)):];
take x;
thus thesis;
end;
consider fs1 be
FinSequence such that
A8: (
dom fs1)
= (
Seg n9) & for k be
Nat st k
in (
Seg n9) holds
P2[k, (fs1
. k)] from
FINSEQ_1:sch 1(
A7);
set u = (
Union (
disjoin fs1));
take u;
A9: (
len fs1)
= (n
- 1) by
A6,
A8,
FINSEQ_1:def 3;
for p be
Nat st p
>= 1 & p
<= (n
- 1) holds (fs1
. p)
=
[:(fs
. p), (fs
. (n
- p)):] by
A8,
A6,
FINSEQ_1: 1;
hence
P[e, u] by
A5,
A9;
end;
end;
consider F be
Function such that
A10: (
dom F)
= ((
bool (
the_universe_of (X
\/
NAT )))
^omega ) & for e be
object st e
in ((
bool (
the_universe_of (X
\/
NAT )))
^omega ) holds
P[e, (F
. e)] from
CLASSES1:sch 1(
A1);
A11: for e be
object st e
in ((
bool (
the_universe_of (X
\/
NAT )))
^omega ) holds (F
. e)
in (
bool (
the_universe_of (X
\/
NAT )))
proof
let e be
object;
assume
A12: e
in ((
bool (
the_universe_of (X
\/
NAT )))
^omega );
then
reconsider fs = e as
XFinSequence of (
bool (
the_universe_of (X
\/
NAT ))) by
AFINSQ_1:def 7;
A13: ((
dom fs)
=
0 implies (F
. e)
=
{} ) & ((
dom fs)
= 1 implies (F
. e)
= X) & for n be
Nat st n
>= 2 & (
dom fs)
= n holds ex fs1 be
FinSequence st (
len fs1)
= (n
- 1) & (for p be
Nat st p
>= 1 & p
<= (n
- 1) holds (fs1
. p)
=
[:(fs
. p), (fs
. (n
- p)):]) & (F
. e)
= (
Union (
disjoin fs1)) by
A12,
A10;
(
dom fs)
=
0 or ((
dom fs)
+ 1)
> (
0
+ 1) by
XREAL_1: 6;
then (
dom fs)
=
0 or (
dom fs)
>= 1 by
NAT_1: 13;
then (
dom fs)
=
0 or (
dom fs)
= 1 or (
dom fs)
> 1 by
XXREAL_0: 1;
then
A14: (
dom fs)
=
0 or (
dom fs)
= 1 or ((
dom fs)
+ 1)
> (1
+ 1) by
XREAL_1: 6;
per cases by
A14,
NAT_1: 13;
suppose
A15: (
dom fs)
=
0 ;
{}
c= (
the_universe_of (X
\/
NAT ));
hence (F
. e)
in (
bool (
the_universe_of (X
\/
NAT ))) by
A15,
A13;
end;
suppose (
dom fs)
= 1;
then
A16: (F
. e)
= X by
A12,
A10;
for x be
object st x
in X holds x
in (
Tarski-Class (
the_transitive-closure_of (X
\/
NAT )))
proof
let x be
object;
reconsider xx = x as
set by
TARSKI: 1;
assume x
in X;
then xx
c= ((
union X)
\/ (
union
NAT )) by
XBOOLE_1: 10,
ZFMISC_1: 74;
then
A17: xx
c= (
union (X
\/
NAT )) by
ZFMISC_1: 78;
A18: (
the_transitive-closure_of (X
\/
NAT ))
in (
Tarski-Class (
the_transitive-closure_of (X
\/
NAT ))) by
CLASSES1: 2;
A19: (
union (X
\/
NAT ))
c= (
union (
the_transitive-closure_of (X
\/
NAT ))) by
CLASSES1: 52,
ZFMISC_1: 77;
(
union (
the_transitive-closure_of (X
\/
NAT )))
c= (
the_transitive-closure_of (X
\/
NAT )) by
CLASSES1: 48,
CLASSES1: 51;
then (
union (X
\/
NAT ))
c= (
the_transitive-closure_of (X
\/
NAT )) by
A19;
hence thesis by
A18,
A17,
CLASSES1: 3,
XBOOLE_1: 1;
end;
then X
c= (
Tarski-Class (
the_transitive-closure_of (X
\/
NAT )));
then X
c= (
the_universe_of (X
\/
NAT )) by
YELLOW_6:def 1;
hence (F
. e)
in (
bool (
the_universe_of (X
\/
NAT ))) by
A16;
end;
suppose
A20: (
dom fs)
>= 2;
set n = (
dom fs);
consider fs1 be
FinSequence such that
A21: (
len fs1)
= (n
- 1) & (for p be
Nat st p
>= 1 & p
<= (n
- 1) holds (fs1
. p)
=
[:(fs
. p), (fs
. (n
- p)):]) & (F
. e)
= (
Union (
disjoin fs1)) by
A20,
A12,
A10;
reconsider n9 = (n
-' 1) as
Nat;
(n
- 1)
>= (2
- 1) by
A20,
XREAL_1: 9;
then
A22: n9
= (n
- 1) by
XREAL_0:def 2;
A23: for p be
Nat st p
>= 1 & p
<= (n
- 1) holds (fs1
. p)
c= (
the_universe_of (X
\/
NAT ))
proof
let p be
Nat;
assume
A24: p
>= 1 & p
<= (n
- 1);
then
A25: (fs1
. p)
=
[:(fs
. p), (fs
. (n
- p)):] by
A21;
A26: p
in (
Seg n9) by
A22,
A24,
FINSEQ_1: 1;
(
- p)
<= (
- 1) & (
- p)
>= (
- (n
- 1)) by
A24,
XREAL_1: 24;
then
A27: ((
- p)
+ n)
<= ((
- 1)
+ n) & ((
- p)
+ n)
>= ((
- (n
- 1))
+ n) by
XREAL_1: 6;
then
A28: (n
- p)
<= (n
-' 1) & (n
- p)
>= 1 by
XREAL_0:def 2;
A29: (n
- p)
= (n
-' p) by
A27,
XREAL_0:def 2;
then
A30: (n
-' p)
in (
Seg n9) by
A28,
FINSEQ_1: 1;
A31: (
Seg n9)
c= (
Segm (n9
+ 1)) by
AFINSQ_1: 3;
then
A32: (fs
. p)
in (
rng fs) by
A26,
A22,
FUNCT_1: 3;
(fs
. (n
- p))
in (
rng fs) by
A29,
A31,
A22,
A30,
FUNCT_1: 3;
hence (fs1
. p)
c= (
the_universe_of (X
\/
NAT )) by
A25,
A32,
Th1;
end;
for x be
set st x
in (
rng (
disjoin fs1)) holds x
c= (
the_universe_of (X
\/
NAT ))
proof
let x be
set;
assume x
in (
rng (
disjoin fs1));
then
consider p be
object such that
A33: p
in (
dom (
disjoin fs1)) & x
= ((
disjoin fs1)
. p) by
FUNCT_1:def 3;
A34: p
in (
dom fs1) by
A33,
CARD_3:def 3;
then
A35: x
=
[:(fs1
. p),
{p}:] by
A33,
CARD_3:def 3;
A36: p
in (
Seg n9) by
A21,
A22,
A34,
FINSEQ_1:def 3;
reconsider p as
Nat by
A34;
p
>= 1 & p
<= (n
- 1) by
A22,
A36,
FINSEQ_1: 1;
then
A37: (fs1
. p)
c= (
the_universe_of (X
\/
NAT )) by
A23;
A38: for y be
set st y
in
{p} holds y
in
NAT
proof
let y be
set;
assume y
in
{p};
then y
= p by
TARSKI:def 1;
hence y
in
NAT by
ORDINAL1:def 12;
end;
for x be
object st x
in
{p} holds x
in (
Tarski-Class (
the_transitive-closure_of (X
\/
NAT )))
proof
let x be
object;
reconsider xx = x as
set by
TARSKI: 1;
assume x
in
{p};
then x
in
NAT by
A38;
then xx
c= ((
union X)
\/ (
union
NAT )) by
XBOOLE_1: 10,
ZFMISC_1: 74;
then
A39: xx
c= (
union (X
\/
NAT )) by
ZFMISC_1: 78;
A40: (
the_transitive-closure_of (X
\/
NAT ))
in (
Tarski-Class (
the_transitive-closure_of (X
\/
NAT ))) by
CLASSES1: 2;
A41: (
union (X
\/
NAT ))
c= (
union (
the_transitive-closure_of (X
\/
NAT ))) by
CLASSES1: 52,
ZFMISC_1: 77;
(
union (
the_transitive-closure_of (X
\/
NAT )))
c= (
the_transitive-closure_of (X
\/
NAT )) by
CLASSES1: 48,
CLASSES1: 51;
then (
union (X
\/
NAT ))
c= (
the_transitive-closure_of (X
\/
NAT )) by
A41;
hence thesis by
A40,
A39,
CLASSES1: 3,
XBOOLE_1: 1;
end;
then
{p}
c= (
Tarski-Class (
the_transitive-closure_of (X
\/
NAT )));
then
{p}
c= (
the_universe_of (X
\/
NAT )) by
YELLOW_6:def 1;
hence thesis by
A35,
A37,
Th1;
end;
then (
union (
rng (
disjoin fs1)))
c= (
the_universe_of (X
\/
NAT )) by
ZFMISC_1: 76;
then (
union (
rng (
disjoin fs1)))
in (
bool (
the_universe_of (X
\/
NAT )));
hence thesis by
A21,
CARD_3:def 4;
end;
end;
::
ALGSTR_4:def13
func
free_magma_seq X ->
sequence of (
bool (
the_universe_of (X
\/
NAT ))) means
:
Def13: (it
.
0 )
=
{} & (it
. 1)
= X & for n be
Nat st n
>= 2 holds ex fs be
FinSequence st (
len fs)
= (n
- 1) & (for p be
Nat st p
>= 1 & p
<= (n
- 1) holds (fs
. p)
=
[:(it
. p), (it
. (n
- p)):]) & (it
. n)
= (
Union (
disjoin fs));
existence
proof
reconsider F as
Function of ((
bool (
the_universe_of (X
\/
NAT )))
^omega ), (
bool (
the_universe_of (X
\/
NAT ))) by
A11,
A10,
FUNCT_2: 3;
deffunc
FX(
XFinSequence of (
bool (
the_universe_of (X
\/
NAT )))) = (F
. $1);
consider f be
sequence of (
bool (
the_universe_of (X
\/
NAT ))) such that
A42: for n be
Nat holds (f
. n)
=
FX(|) from
FuncRecursiveExist2;
take f;
A43:
{}
in ((
bool (
the_universe_of (X
\/
NAT )))
^omega ) by
AFINSQ_1: 43;
A44: (
dom
{} )
=
{} ;
thus (f
.
0 )
= (F
. (f
|
{} )) by
A42
.=
{} by
A43,
A44,
A10;
1
c=
NAT ;
then 1
c= (
dom f) by
FUNCT_2:def 1;
then
A45: (
dom (f
| 1))
= 1 by
RELAT_1: 62;
A46: (f
| 1)
in ((
bool (
the_universe_of (X
\/
NAT )))
^omega ) by
AFINSQ_1: 42;
thus (f
. 1)
= (F
. (f
| 1)) by
A42
.= X by
A45,
A46,
A10;
let n be
Nat;
assume
A47: n
>= 2;
n
c=
NAT ;
then n
c= (
dom f) by
FUNCT_2:def 1;
then
A48: (
dom (f
| n))
= n by
RELAT_1: 62;
(f
| n)
in ((
bool (
the_universe_of (X
\/
NAT )))
^omega ) by
AFINSQ_1: 42;
then
consider fs1 be
FinSequence such that
A49: (
len fs1)
= (n
- 1) & (for p be
Nat st p
>= 1 & p
<= (n
- 1) holds (fs1
. p)
=
[:((f
| n)
. p), ((f
| n)
. (n
- p)):]) & (F
. (f
| n))
= (
Union (
disjoin fs1)) by
A47,
A48,
A10;
take fs1;
thus (
len fs1)
= (n
- 1) by
A49;
thus for p be
Nat st p
>= 1 & p
<= (n
- 1) holds (fs1
. p)
=
[:(f
. p), (f
. (n
- p)):]
proof
let p be
Nat;
assume
A50: p
>= 1 & p
<= (n
- 1);
set n9 = (n
-' 1);
(n
- 1)
>= (2
- 1) by
A47,
XREAL_1: 9;
then
A51: n9
= (n
- 1) by
XREAL_0:def 2;
then
A52: p
in (
Seg n9) by
A50,
FINSEQ_1: 1;
(
Seg n9)
c= (
Segm (n9
+ 1)) by
AFINSQ_1: 3;
then
A53: ((f
| n)
. p)
= (f
. p) by
A51,
A52,
FUNCT_1: 49;
(
- p)
<= (
- 1) & (
- p)
>= (
- (n
- 1)) by
A50,
XREAL_1: 24;
then
A54: ((
- p)
+ n)
<= ((
- 1)
+ n) & ((
- p)
+ n)
>= ((
- (n
- 1))
+ n) by
XREAL_1: 6;
then
A55: (n
- p)
<= (n
-' 1) & (n
- p)
>= 1 by
XREAL_0:def 2;
A56: (n
- p)
= (n
-' p) by
A54,
XREAL_0:def 2;
then
A57: (n
-' p)
in (
Seg n9) by
A55,
FINSEQ_1: 1;
A58: (
Seg n9)
c= (
Segm (n9
+ 1)) by
AFINSQ_1: 3;
thus (fs1
. p)
=
[:((f
| n)
. p), ((f
| n)
. (n
- p)):] by
A50,
A49
.=
[:(f
. p), (f
. (n
- p)):] by
A53,
A58,
A56,
A51,
A57,
FUNCT_1: 49;
end;
thus (f
. n)
= (
Union (
disjoin fs1)) by
A49,
A42;
end;
uniqueness
proof
let f1,f2 be
sequence of (
bool (
the_universe_of (X
\/
NAT )));
assume
A59: (f1
.
0 )
=
{} ;
assume
A60: (f1
. 1)
= X;
assume
A61: for n be
Nat st n
>= 2 holds ex fs be
FinSequence st (
len fs)
= (n
- 1) & (for p be
Nat st p
>= 1 & p
<= (n
- 1) holds (fs
. p)
=
[:(f1
. p), (f1
. (n
- p)):]) & (f1
. n)
= (
Union (
disjoin fs));
assume
A62: (f2
.
0 )
=
{} ;
assume
A63: (f2
. 1)
= X;
assume
A64: for n be
Nat st n
>= 2 holds ex fs be
FinSequence st (
len fs)
= (n
- 1) & (for p be
Nat st p
>= 1 & p
<= (n
- 1) holds (fs
. p)
=
[:(f2
. p), (f2
. (n
- p)):]) & (f2
. n)
= (
Union (
disjoin fs));
{}
in ((
bool (
the_universe_of (X
\/
NAT )))
^omega ) by
AFINSQ_1: 43;
then
A65:
P[
{} , (F
.
{} )] &
{} is
XFinSequence of (
bool (
the_universe_of (X
\/
NAT ))) by
A10,
AFINSQ_1: 42;
A66: (
dom
{} )
=
{} ;
reconsider F as
Function of ((
bool (
the_universe_of (X
\/
NAT )))
^omega ), (
bool (
the_universe_of (X
\/
NAT ))) by
A11,
A10,
FUNCT_2: 3;
deffunc
FX(
XFinSequence of (
bool (
the_universe_of (X
\/
NAT )))) = (F
. $1);
A67: for n be
Nat holds (f1
. n)
=
FX(|)
proof
let n be
Nat;
n
=
0 or (n
+ 1)
> (
0
+ 1) by
XREAL_1: 6;
then n
=
0 or n
>= 1 by
NAT_1: 13;
then n
=
0 or n
= 1 or n
> 1 by
XXREAL_0: 1;
then
A68: n
=
0 or n
= 1 or (n
+ 1)
> (1
+ 1) by
XREAL_1: 6;
per cases by
A68,
NAT_1: 13;
suppose
A69: n
=
0 ;
hence (f1
. n)
= (F
.
{} ) by
A65,
A66,
A59
.=
FX(|) by
A69;
end;
suppose
A70: n
= 1;
1
c=
NAT ;
then 1
c= (
dom f1) by
FUNCT_2:def 1;
then
A71: (
dom (f1
| 1))
= 1 by
RELAT_1: 62;
(f1
| 1)
in ((
bool (
the_universe_of (X
\/
NAT )))
^omega ) by
AFINSQ_1: 42;
hence (f1
. n)
=
FX(|) by
A70,
A71,
A10,
A60;
end;
suppose
A72: n
>= 2;
n
c=
NAT ;
then n
c= (
dom f1) by
FUNCT_2:def 1;
then
A73: (
dom (f1
| n))
= n by
RELAT_1: 62;
(f1
| n)
in ((
bool (
the_universe_of (X
\/
NAT )))
^omega ) by
AFINSQ_1: 42;
then
consider fs1 be
FinSequence such that
A74: (
len fs1)
= (n
- 1) & (for p be
Nat st p
>= 1 & p
<= (n
- 1) holds (fs1
. p)
=
[:((f1
| n)
. p), ((f1
| n)
. (n
- p)):]) & (F
. (f1
| n))
= (
Union (
disjoin fs1)) by
A72,
A73,
A10;
consider fs2 be
FinSequence such that
A75: (
len fs2)
= (n
- 1) & (for p be
Nat st p
>= 1 & p
<= (n
- 1) holds (fs2
. p)
=
[:(f1
. p), (f1
. (n
- p)):]) & (f1
. n)
= (
Union (
disjoin fs2)) by
A72,
A61;
for p be
Nat st 1
<= p & p
<= (
len fs1) holds (fs1
. p)
= (fs2
. p)
proof
let p be
Nat;
assume
A76: 1
<= p & p
<= (
len fs1);
then
A77: (fs1
. p)
=
[:((f1
| n)
. p), ((f1
| n)
. (n
- p)):] by
A74;
A78: (fs2
. p)
=
[:(f1
. p), (f1
. (n
- p)):] by
A76,
A74,
A75;
set n9 = (n
-' 1);
(n
- 1)
>= (2
- 1) by
A72,
XREAL_1: 9;
then
A79: n9
= (n
- 1) by
XREAL_0:def 2;
then
A80: p
in (
Seg n9) by
A76,
A74,
FINSEQ_1: 1;
A81: (
Seg n9)
c= (
Segm (n9
+ 1)) by
AFINSQ_1: 3;
(
- p)
<= (
- 1) & (
- p)
>= (
- (n
- 1)) by
A76,
A74,
XREAL_1: 24;
then
A82: ((
- p)
+ n)
<= ((
- 1)
+ n) & ((
- p)
+ n)
>= ((
- (n
- 1))
+ n) by
XREAL_1: 6;
then
A83: (n
- p)
<= (n
-' 1) & (n
- p)
>= 1 by
XREAL_0:def 2;
A84: (n
- p)
= (n
-' p) by
A82,
XREAL_0:def 2;
then
A85: (n
-' p)
in (
Seg n9) by
A83,
FINSEQ_1: 1;
(
Seg n9)
c= (
Segm (n9
+ 1)) by
AFINSQ_1: 3;
then ((f1
| n)
. (n
- p))
= (f1
. (n
- p)) by
A84,
A79,
A85,
FUNCT_1: 49;
hence (fs1
. p)
= (fs2
. p) by
A81,
A77,
A78,
A79,
A80,
FUNCT_1: 49;
end;
hence (f1
. n)
=
FX(|) by
A74,
A75,
FINSEQ_1: 14;
end;
end;
A86: for n be
Nat holds (f2
. n)
=
FX(|)
proof
let n be
Nat;
n
=
0 or (n
+ 1)
> (
0
+ 1) by
XREAL_1: 6;
then n
=
0 or n
>= 1 by
NAT_1: 13;
then n
=
0 or n
= 1 or n
> 1 by
XXREAL_0: 1;
then
A87: n
=
0 or n
= 1 or (n
+ 1)
> (1
+ 1) by
XREAL_1: 6;
per cases by
A87,
NAT_1: 13;
suppose
A88: n
=
0 ;
hence (f2
. n)
= (F
.
{} ) by
A65,
A66,
A62
.=
FX(|) by
A88;
end;
suppose
A89: n
= 1;
1
c=
NAT ;
then 1
c= (
dom f2) by
FUNCT_2:def 1;
then
A90: (
dom (f2
| 1))
= 1 by
RELAT_1: 62;
(f2
| 1)
in ((
bool (
the_universe_of (X
\/
NAT )))
^omega ) by
AFINSQ_1: 42;
hence (f2
. n)
=
FX(|) by
A90,
A10,
A89,
A63;
end;
suppose
A91: n
>= 2;
n
c=
NAT ;
then n
c= (
dom f2) by
FUNCT_2:def 1;
then
A92: (
dom (f2
| n))
= n by
RELAT_1: 62;
(f2
| n)
in ((
bool (
the_universe_of (X
\/
NAT )))
^omega ) by
AFINSQ_1: 42;
then
consider fs1 be
FinSequence such that
A93: (
len fs1)
= (n
- 1) & (for p be
Nat st p
>= 1 & p
<= (n
- 1) holds (fs1
. p)
=
[:((f2
| n)
. p), ((f2
| n)
. (n
- p)):]) & (F
. (f2
| n))
= (
Union (
disjoin fs1)) by
A91,
A92,
A10;
consider fs2 be
FinSequence such that
A94: (
len fs2)
= (n
- 1) & (for p be
Nat st p
>= 1 & p
<= (n
- 1) holds (fs2
. p)
=
[:(f2
. p), (f2
. (n
- p)):]) & (f2
. n)
= (
Union (
disjoin fs2)) by
A91,
A64;
for p be
Nat st 1
<= p & p
<= (
len fs1) holds (fs1
. p)
= (fs2
. p)
proof
let p be
Nat;
assume
A95: 1
<= p & p
<= (
len fs1);
then
A96: (fs1
. p)
=
[:((f2
| n)
. p), ((f2
| n)
. (n
- p)):] by
A93;
A97: (fs2
. p)
=
[:(f2
. p), (f2
. (n
- p)):] by
A95,
A93,
A94;
set n9 = (n
-' 1);
(n
- 1)
>= (2
- 1) by
A91,
XREAL_1: 9;
then
A98: n9
= (n
- 1) by
XREAL_0:def 2;
then
A99: p
in (
Seg n9) by
A95,
A93,
FINSEQ_1: 1;
A100: (
Seg n9)
c= (
Segm (n9
+ 1)) by
AFINSQ_1: 3;
(
- p)
<= (
- 1) & (
- p)
>= (
- (n
- 1)) by
A95,
A93,
XREAL_1: 24;
then
A101: ((
- p)
+ n)
<= ((
- 1)
+ n) & ((
- p)
+ n)
>= ((
- (n
- 1))
+ n) by
XREAL_1: 6;
then
A102: (n
- p)
<= (n
-' 1) & (n
- p)
>= 1 by
XREAL_0:def 2;
A103: (n
- p)
= (n
-' p) by
A101,
XREAL_0:def 2;
then
A104: (n
-' p)
in (
Seg n9) by
A102,
FINSEQ_1: 1;
(
Seg n9)
c= (
Segm (n9
+ 1)) by
AFINSQ_1: 3;
then ((f2
| n)
. (n
- p))
= (f2
. (n
- p)) by
A104,
A103,
A98,
FUNCT_1: 49;
hence (fs1
. p)
= (fs2
. p) by
A100,
A96,
A97,
A98,
A99,
FUNCT_1: 49;
end;
hence (f2
. n)
=
FX(|) by
A94,
A93,
FINSEQ_1: 14;
end;
end;
f1
= f2 from
FuncRecursiveUniqu2(
A67,
A86);
hence thesis;
end;
end
definition
let X be
set;
let n be
Nat;
::
ALGSTR_4:def14
func
free_magma (X,n) ->
set equals ((
free_magma_seq X)
. n);
correctness ;
end
registration
let X be non
empty
set;
let n be non
zero
Nat;
cluster (
free_magma (X,n)) -> non
empty;
correctness
proof
defpred
P[
Nat] means $1
=
0 or ((
free_magma_seq X)
. $1)
<>
{} ;
A1: for k be
Nat st for n be
Nat st n
< k holds
P[n] holds
P[k]
proof
let k be
Nat;
assume
A2: for n be
Nat st n
< k holds
P[n];
k
=
0 or (k
+ 1)
> (
0
+ 1) by
XREAL_1: 6;
then k
=
0 or k
>= 1 by
NAT_1: 13;
then k
=
0 or k
= 1 or k
> 1 by
XXREAL_0: 1;
then
A3: k
=
0 or k
= 1 or (k
+ 1)
> (1
+ 1) by
XREAL_1: 6;
per cases by
A3,
NAT_1: 13;
suppose k
=
0 ;
hence
P[k];
end;
suppose k
= 1;
hence
P[k] by
Def13;
end;
suppose
A4: k
>= 2;
then
consider fs be
FinSequence such that
A5: (
len fs)
= (k
- 1) & (for p be
Nat st p
>= 1 & p
<= (k
- 1) holds (fs
. p)
=
[:((
free_magma_seq X)
. p), ((
free_magma_seq X)
. (k
- p)):]) & ((
free_magma_seq X)
. k)
= (
Union (
disjoin fs)) by
Def13;
A6: (2
- 1)
<= (k
- 1) by
A4,
XREAL_1: 9;
then 1
in (
Seg (
len fs)) by
A5,
FINSEQ_1: 1;
then
A7: 1
in (
dom fs) by
FINSEQ_1:def 3;
then
A8: 1
in (
dom (
disjoin fs)) by
CARD_3:def 3;
A9: ((
disjoin fs)
. 1)
=
[:(fs
. 1),
{1}:] by
A7,
CARD_3:def 3;
A10: (fs
. 1)
=
[:((
free_magma_seq X)
. 1), ((
free_magma_seq X)
. (k
- 1)):] by
A5,
A6;
(1
+ 1)
<= ((k
- 1)
+ 1) by
A4;
then 1
< k by
NAT_1: 13;
then
A11: ((
free_magma_seq X)
. 1)
<>
{} by
A2;
A12: ((
- 1)
+ k)
< (
0
+ k) by
XREAL_1: 8;
(k
- 1)
in
NAT by
A6,
INT_1: 3;
then
reconsider k9 = (k
- 1) as
Nat;
((
free_magma_seq X)
. k9)
<>
{} by
A12,
A6,
A2;
then
consider x be
object such that
A13: x
in
[:(fs
. 1),
{1}:] by
A11,
A10,
XBOOLE_0:def 1;
[:(fs
. 1),
{1}:]
c= (
union (
rng (
disjoin fs))) by
A9,
A8,
FUNCT_1: 3,
ZFMISC_1: 74;
hence
P[k] by
A13,
A5,
CARD_3:def 4;
end;
end;
for n be
Nat holds
P[n] from
NAT_1:sch 4(
A1);
hence thesis;
end;
end
reserve X for
set;
theorem ::
ALGSTR_4:16
(
free_magma (X,
0 ))
=
{} by
Def13;
theorem ::
ALGSTR_4:17
(
free_magma (X,1))
= X by
Def13;
theorem ::
ALGSTR_4:18
Th18: (
free_magma (X,2))
=
[:
[:X, X:],
{1}:]
proof
consider fs be
FinSequence such that
A1: (
len fs)
= (2
- 1) & (for p be
Nat st p
>= 1 & p
<= (2
- 1) holds (fs
. p)
=
[:((
free_magma_seq X)
. p), ((
free_magma_seq X)
. (2
- p)):]) & ((
free_magma_seq X)
. 2)
= (
Union (
disjoin fs)) by
Def13;
A2: (fs
. 1)
=
[:((
free_magma_seq X)
. 1), ((
free_magma_seq X)
. (2
- 1)):] by
A1
.=
[:(
free_magma (X,1)), X:] by
Def13
.=
[:X, X:] by
Def13;
then
A3: fs
=
<*
[:X, X:]*> by
A1,
FINSEQ_1: 40;
A4: for y be
object holds y
in (
union (
rng (
disjoin fs))) iff y
in
[:
[:X, X:],
{1}:]
proof
let y be
object;
hereby
assume y
in (
union (
rng (
disjoin fs)));
then
consider Y be
set such that
A5: y
in Y & Y
in (
rng (
disjoin fs)) by
TARSKI:def 4;
consider x be
object such that
A6: x
in (
dom (
disjoin fs)) & Y
= ((
disjoin fs)
. x) by
A5,
FUNCT_1:def 3;
A7: x
in (
dom fs) by
A6,
CARD_3:def 3;
then x
in (
Seg 1) by
A3,
FINSEQ_1: 38;
then x
= 1 by
FINSEQ_1: 2,
TARSKI:def 1;
hence y
in
[:
[:X, X:],
{1}:] by
A5,
A2,
A6,
A7,
CARD_3:def 3;
end;
assume
A8: y
in
[:
[:X, X:],
{1}:];
1
in (
Seg 1) by
FINSEQ_1: 1;
then
A9: 1
in (
dom fs) by
A3,
FINSEQ_1: 38;
then
A10: 1
in (
dom (
disjoin fs)) by
CARD_3:def 3;
[:
[:X, X:],
{1}:]
= ((
disjoin fs)
. 1) by
A2,
A9,
CARD_3:def 3;
then
[:
[:X, X:],
{1}:]
in (
rng (
disjoin fs)) by
A10,
FUNCT_1:def 3;
hence y
in (
union (
rng (
disjoin fs))) by
A8,
TARSKI:def 4;
end;
thus (
free_magma (X,2))
= (
union (
rng (
disjoin fs))) by
A1,
CARD_3:def 4
.=
[:
[:X, X:],
{1}:] by
A4,
TARSKI: 2;
end;
theorem ::
ALGSTR_4:19
(
free_magma (X,3))
= (
[:
[:X,
[:
[:X, X:],
{1}:]:],
{1}:]
\/
[:
[:
[:
[:X, X:],
{1}:], X:],
{2}:])
proof
set X1 =
[:
[:X,
[:
[:X, X:],
{1}:]:],
{1}:];
set X2 =
[:
[:
[:
[:X, X:],
{1}:], X:],
{2}:];
consider fs be
FinSequence such that
A1: (
len fs)
= (3
- 1) & (for p be
Nat st p
>= 1 & p
<= (3
- 1) holds (fs
. p)
=
[:((
free_magma_seq X)
. p), ((
free_magma_seq X)
. (3
- p)):]) & ((
free_magma_seq X)
. 3)
= (
Union (
disjoin fs)) by
Def13;
A2: (fs
. 1)
=
[:(
free_magma (X,1)), (
free_magma (X,2)):] by
A1
.=
[:(
free_magma (X,1)),
[:
[:X, X:],
{1}:]:] by
Th18
.=
[:X,
[:
[:X, X:],
{1}:]:] by
Def13;
A3: (fs
. 2)
=
[:((
free_magma_seq X)
. 2), ((
free_magma_seq X)
. (3
- 2)):] by
A1
.=
[:(
free_magma (X,2)), X:] by
Def13
.=
[:
[:
[:X, X:],
{1}:], X:] by
Th18;
A4: for y be
object holds y
in (
union (
rng (
disjoin fs))) iff y
in X1 or y
in X2
proof
let y be
object;
hereby
assume y
in (
union (
rng (
disjoin fs)));
then
consider Y be
set such that
A5: y
in Y & Y
in (
rng (
disjoin fs)) by
TARSKI:def 4;
consider x be
object such that
A6: x
in (
dom (
disjoin fs)) & Y
= ((
disjoin fs)
. x) by
A5,
FUNCT_1:def 3;
A7: x
in (
dom fs) by
A6,
CARD_3:def 3;
then x
in
{1, 2} by
A1,
FINSEQ_1: 2,
FINSEQ_1:def 3;
then x
= 1 or x
= 2 by
TARSKI:def 2;
hence y
in X1 or y
in X2 by
A2,
A3,
A5,
A6,
A7,
CARD_3:def 3;
end;
assume
A8: y
in X1 or y
in X2;
1
in (
Seg 2) & 2
in (
Seg 2) by
FINSEQ_1: 1;
then
A9: 1
in (
dom fs) & 2
in (
dom fs) by
A1,
FINSEQ_1:def 3;
then
A10: 1
in (
dom (
disjoin fs)) & 2
in (
dom (
disjoin fs)) by
CARD_3:def 3;
X1
= ((
disjoin fs)
. 1) & X2
= ((
disjoin fs)
. 2) by
A2,
A3,
A9,
CARD_3:def 3;
then X1
in (
rng (
disjoin fs)) & X2
in (
rng (
disjoin fs)) by
A10,
FUNCT_1:def 3;
hence y
in (
union (
rng (
disjoin fs))) by
A8,
TARSKI:def 4;
end;
thus (
free_magma (X,3))
= (
union (
rng (
disjoin fs))) by
A1,
CARD_3:def 4
.= (
[:
[:X,
[:
[:X, X:],
{1}:]:],
{1}:]
\/
[:
[:
[:
[:X, X:],
{1}:], X:],
{2}:]) by
A4,
XBOOLE_0:def 3;
end;
reserve x,y,Y for
set;
reserve n,m,p for
Nat;
theorem ::
ALGSTR_4:20
Th20: n
>= 2 implies ex fs be
FinSequence st (
len fs)
= (n
- 1) & (for p st p
>= 1 & p
<= (n
- 1) holds (fs
. p)
=
[:(
free_magma (X,p)), (
free_magma (X,(n
-' p))):]) & (
free_magma (X,n))
= (
Union (
disjoin fs))
proof
assume n
>= 2;
then
consider fs be
FinSequence such that
A1: (
len fs)
= (n
- 1) & (for p st p
>= 1 & p
<= (n
- 1) holds (fs
. p)
=
[:((
free_magma_seq X)
. p), ((
free_magma_seq X)
. (n
- p)):]) & ((
free_magma_seq X)
. n)
= (
Union (
disjoin fs)) by
Def13;
take fs;
thus (
len fs)
= (n
- 1) by
A1;
thus for p st p
>= 1 & p
<= (n
- 1) holds (fs
. p)
=
[:(
free_magma (X,p)), (
free_magma (X,(n
-' p))):]
proof
let p;
assume
A2: p
>= 1 & p
<= (n
- 1);
then (
- p)
<= (
- 1) & (
- p)
>= (
- (n
- 1)) by
XREAL_1: 24;
then ((
- p)
+ n)
<= ((
- 1)
+ n) & ((
- p)
+ n)
>= ((
- (n
- 1))
+ n) by
XREAL_1: 6;
then (n
- p)
= (n
-' p) by
XREAL_0:def 2;
hence thesis by
A2,
A1;
end;
thus (
free_magma (X,n))
= (
Union (
disjoin fs)) by
A1;
end;
theorem ::
ALGSTR_4:21
Th21: n
>= 2 & x
in (
free_magma (X,n)) implies ex p, m st (x
`2 )
= p & 1
<= p & p
<= (n
- 1) & ((x
`1 )
`1 )
in (
free_magma (X,p)) & ((x
`1 )
`2 )
in (
free_magma (X,m)) & n
= (p
+ m) & x
in
[:
[:(
free_magma (X,p)), (
free_magma (X,m)):],
{p}:]
proof
assume
A1: n
>= 2;
assume
A2: x
in (
free_magma (X,n));
consider fs be
FinSequence such that
A3: (
len fs)
= (n
- 1) and
A4: (for p st p
>= 1 & p
<= (n
- 1) holds (fs
. p)
=
[:((
free_magma_seq X)
. p), ((
free_magma_seq X)
. (n
- p)):]) and
A5: ((
free_magma_seq X)
. n)
= (
Union (
disjoin fs)) by
A1,
Def13;
x
in (
union (
rng (
disjoin fs))) by
A2,
A5,
CARD_3:def 4;
then
consider Y be
set such that
A6: x
in Y & Y
in (
rng (
disjoin fs)) by
TARSKI:def 4;
consider p be
object such that
A7: p
in (
dom (
disjoin fs)) & Y
= ((
disjoin fs)
. p) by
A6,
FUNCT_1:def 3;
A8: p
in (
dom fs) by
A7,
CARD_3:def 3;
then
reconsider p as
Nat;
A9: p
in (
Seg (
len fs)) by
A8,
FINSEQ_1:def 3;
then
A10: 1
<= p & p
<= (
len fs) by
FINSEQ_1: 1;
then
A11: (fs
. p)
=
[:((
free_magma_seq X)
. p), ((
free_magma_seq X)
. (n
- p)):] by
A3,
A4;
then x
in
[:
[:((
free_magma_seq X)
. p), ((
free_magma_seq X)
. (n
- p)):],
{p}:] by
A6,
A7,
A8,
CARD_3:def 3;
then
A12: (x
`1 )
in
[:((
free_magma_seq X)
. p), ((
free_magma_seq X)
. (n
- p)):] & (x
`2 )
in
{p} by
MCART_1: 10;
(
- p)
>= (
- (n
- 1)) by
A10,
A3,
XREAL_1: 24;
then ((
- p)
+ n)
>= ((
- (n
- 1))
+ n) by
XREAL_1: 7;
then (n
- p)
in
NAT by
INT_1: 3;
then
reconsider m = (n
- p) as
Nat;
take p, m;
thus thesis by
A3,
A9,
A6,
A11,
A7,
A8,
A12,
CARD_3:def 3,
FINSEQ_1: 1,
MCART_1: 10,
TARSKI:def 1;
end;
theorem ::
ALGSTR_4:22
Th22: x
in (
free_magma (X,n)) & y
in (
free_magma (X,m)) implies
[
[x, y], n]
in (
free_magma (X,(n
+ m)))
proof
assume
A1: x
in (
free_magma (X,n));
assume
A2: y
in (
free_magma (X,m));
per cases ;
suppose n
=
0 or m
=
0 ;
hence thesis by
Def13,
A1,
A2;
end;
suppose n
<>
0 & m
<>
0 ;
then
A3: n
>= (
0
+ 1) & m
>= (
0
+ 1) by
NAT_1: 13;
then (n
+ m)
>= (1
+ 1) by
XREAL_1: 7;
then
consider fs be
FinSequence such that
A4: (
len fs)
= ((n
+ m)
- 1) & (for p st p
>= 1 & p
<= ((n
+ m)
- 1) holds (fs
. p)
=
[:((
free_magma_seq X)
. p), ((
free_magma_seq X)
. ((n
+ m)
- p)):]) & ((
free_magma_seq X)
. (n
+ m))
= (
Union (
disjoin fs)) by
Def13;
(1
- 1)
<= (m
- 1) by
A3,
XREAL_1: 9;
then
A5: (
0
+ n)
<= ((m
- 1)
+ n) by
XREAL_1: 7;
then (fs
. n)
=
[:((
free_magma_seq X)
. n), ((
free_magma_seq X)
. ((n
+ m)
- n)):] by
A4,
A3
.=
[:((
free_magma_seq X)
. n), ((
free_magma_seq X)
. m):];
then
A6:
[x, y]
in (fs
. n) by
A1,
A2,
ZFMISC_1:def 2;
n
in
{n} by
TARSKI:def 1;
then
A7:
[
[x, y], n]
in
[:(fs
. n),
{n}:] by
A6,
ZFMISC_1:def 2;
n
in (
Seg (
len fs)) by
A4,
A3,
A5,
FINSEQ_1: 1;
then
A8: n
in (
dom fs) by
FINSEQ_1:def 3;
then
A9: ((
disjoin fs)
. n)
=
[:(fs
. n),
{n}:] by
CARD_3:def 3;
n
in (
dom (
disjoin fs)) by
A8,
CARD_3:def 3;
then
[:(fs
. n),
{n}:]
in (
rng (
disjoin fs)) by
A9,
FUNCT_1: 3;
then
[
[x, y], n]
in (
union (
rng (
disjoin fs))) by
A7,
TARSKI:def 4;
hence
[
[x, y], n]
in (
free_magma (X,(n
+ m))) by
A4,
CARD_3:def 4;
end;
end;
theorem ::
ALGSTR_4:23
Th23: X
c= Y implies (
free_magma (X,n))
c= (
free_magma (Y,n))
proof
defpred
P[
Nat] means X
c= Y implies (
free_magma (X,$1))
c= (
free_magma (Y,$1));
A1: for k be
Nat st for n be
Nat st n
< k holds
P[n] holds
P[k]
proof
let k be
Nat;
assume
A2: for n be
Nat st n
< k holds
P[n];
thus X
c= Y implies (
free_magma (X,k))
c= (
free_magma (Y,k))
proof
assume
A3: X
c= Y;
k
=
0 or (k
+ 1)
> (
0
+ 1) by
XREAL_1: 6;
then k
=
0 or k
>= 1 by
NAT_1: 13;
then k
=
0 or k
= 1 or k
> 1 by
XXREAL_0: 1;
then
A4: k
=
0 or k
= 1 or (k
+ 1)
> (1
+ 1) by
XREAL_1: 6;
per cases by
A4,
NAT_1: 13;
suppose k
=
0 ;
then (
free_magma (X,k))
=
{} & (
free_magma (Y,k))
=
{} by
Def13;
hence (
free_magma (X,k))
c= (
free_magma (Y,k));
end;
suppose k
= 1;
then (
free_magma (X,k))
= X & (
free_magma (Y,k))
= Y by
Def13;
hence (
free_magma (X,k))
c= (
free_magma (Y,k)) by
A3;
end;
suppose
A5: k
>= 2;
for x be
object st x
in (
free_magma (X,k)) holds x
in (
free_magma (Y,k))
proof
let x be
object;
assume x
in (
free_magma (X,k));
then
consider p,m be
Nat such that
A6: (x
`2 )
= p & 1
<= p & p
<= (k
- 1) & ((x
`1 )
`1 )
in (
free_magma (X,p)) & ((x
`1 )
`2 )
in (
free_magma (X,m)) & k
= (p
+ m) & x
in
[:
[:(
free_magma (X,p)), (
free_magma (X,m)):],
{p}:] by
A5,
Th21;
consider fs be
FinSequence such that
A7: (
len fs)
= (k
- 1) & (for p be
Nat st p
>= 1 & p
<= (k
- 1) holds (fs
. p)
=
[:(
free_magma (Y,p)), (
free_magma (Y,(k
-' p))):]) & (
free_magma (Y,k))
= (
Union (
disjoin fs)) by
A5,
Th20;
A8: (fs
. p)
=
[:(
free_magma (Y,p)), (
free_magma (Y,(k
-' p))):] by
A6,
A7;
A9: (x
`1 )
in
[:(
free_magma (X,p)), (
free_magma (X,m)):] & (x
`2 )
in
{p} by
A6,
MCART_1: 10;
A10: x
=
[(x
`1 ), (x
`2 )] by
A6,
MCART_1: 21;
A11: (x
`1 )
=
[((x
`1 )
`1 ), ((x
`1 )
`2 )] by
A9,
MCART_1: 21;
(p
+ 1)
<= ((k
- 1)
+ 1) by
A6,
XREAL_1: 7;
then
A12: p
< k by
NAT_1: 13;
then
A13: (
free_magma (X,p))
c= (
free_magma (Y,p)) by
A2,
A3;
(p
- p)
< (k
- p) by
A12,
XREAL_1: 14;
then
A14: (k
-' p)
= m by
A6,
XREAL_0:def 2;
(p
+ m)
> (
0
+ m) by
A6,
XREAL_1: 8;
then (
free_magma (X,m))
c= (
free_magma (Y,(k
-' p))) by
A6,
A2,
A3,
A14;
then (x
`1 )
in
[:(
free_magma (Y,p)), (
free_magma (Y,(k
-' p))):] by
A6,
A11,
A13,
ZFMISC_1:def 2;
then
A15: x
in
[:(fs
. p),
{p}:] by
A8,
A10,
A9,
ZFMISC_1:def 2;
p
in (
Seg (
len fs)) by
A6,
A7,
FINSEQ_1: 1;
then
A16: p
in (
dom fs) by
FINSEQ_1:def 3;
then
A17: ((
disjoin fs)
. p)
=
[:(fs
. p),
{p}:] by
CARD_3:def 3;
p
in (
dom (
disjoin fs)) by
A16,
CARD_3:def 3;
then
[:(fs
. p),
{p}:]
in (
rng (
disjoin fs)) by
A17,
FUNCT_1: 3;
then x
in (
union (
rng (
disjoin fs))) by
A15,
TARSKI:def 4;
hence x
in (
free_magma (Y,k)) by
A7,
CARD_3:def 4;
end;
hence (
free_magma (X,k))
c= (
free_magma (Y,k));
end;
end;
end;
for k be
Nat holds
P[k] from
NAT_1:sch 4(
A1);
hence thesis;
end;
definition
let X be
set;
::
ALGSTR_4:def15
func
free_magma_carrier X ->
set equals (
Union (
disjoin ((
free_magma_seq X)
|
NATPLUS )));
correctness ;
end
Lm1: n
>
0 implies
[:(
free_magma (X,n)),
{n}:]
c= (
free_magma_carrier X)
proof
assume
A1: n
>
0 ;
let x be
object;
assume
A2: x
in
[:(
free_magma (X,n)),
{n}:];
n
in
NAT by
ORDINAL1:def 12;
then
A3: n
in (
dom (
free_magma_seq X)) by
FUNCT_2:def 1;
n
in
NATPLUS by
A1,
NAT_LAT:def 6;
then
A4: n
in (
dom ((
free_magma_seq X)
|
NATPLUS )) by
A3,
RELAT_1: 57;
then
A5: ((
disjoin ((
free_magma_seq X)
|
NATPLUS ))
. n)
=
[:(((
free_magma_seq X)
|
NATPLUS )
. n),
{n}:] by
CARD_3:def 3
.=
[:((
free_magma_seq X)
. n),
{n}:] by
A4,
FUNCT_1: 47;
n
in (
dom (
disjoin ((
free_magma_seq X)
|
NATPLUS ))) by
A4,
CARD_3:def 3;
then
[:(
free_magma (X,n)),
{n}:]
in (
rng (
disjoin ((
free_magma_seq X)
|
NATPLUS ))) by
A5,
FUNCT_1: 3;
then x
in (
union (
rng (
disjoin ((
free_magma_seq X)
|
NATPLUS )))) by
A2,
TARSKI:def 4;
hence x
in (
free_magma_carrier X) by
CARD_3:def 4;
end;
theorem ::
ALGSTR_4:24
Th24: X
=
{} iff (
free_magma_carrier X)
=
{}
proof
hereby
assume
A1: X
=
{} ;
defpred
P[
Nat] means ((
free_magma_seq X)
. $1)
=
{} ;
A2: for k be
Nat st for n be
Nat st n
< k holds
P[n] holds
P[k]
proof
let k be
Nat;
assume
A3: for n be
Nat st n
< k holds
P[n];
k
=
0 or (k
+ 1)
> (
0
+ 1) by
XREAL_1: 6;
then k
=
0 or k
>= 1 by
NAT_1: 13;
then k
=
0 or k
= 1 or k
> 1 by
XXREAL_0: 1;
then
A4: k
=
0 or k
= 1 or (k
+ 1)
> (1
+ 1) by
XREAL_1: 6;
per cases by
A4,
NAT_1: 13;
suppose k
=
0 ;
hence
P[k] by
Def13;
end;
suppose k
= 1;
hence
P[k] by
A1,
Def13;
end;
suppose k
>= 2;
then
consider fs be
FinSequence such that
A5: (
len fs)
= (k
- 1) & (for p be
Nat st p
>= 1 & p
<= (k
- 1) holds (fs
. p)
=
[:((
free_magma_seq X)
. p), ((
free_magma_seq X)
. (k
- p)):]) & ((
free_magma_seq X)
. k)
= (
Union (
disjoin fs)) by
Def13;
for y be
set st y
in (
rng (
disjoin fs)) holds y
c=
{}
proof
let y be
set;
assume y
in (
rng (
disjoin fs));
then
consider p be
object such that
A6: p
in (
dom (
disjoin fs)) & y
= ((
disjoin fs)
. p) by
FUNCT_1:def 3;
A7: p
in (
dom fs) by
A6,
CARD_3:def 3;
then
A8: p
in (
Seg (
len fs)) by
FINSEQ_1:def 3;
reconsider p as
Nat by
A7;
A9: p
>= 1 & p
<= (k
- 1) by
A5,
A8,
FINSEQ_1: 1;
then (p
+ 1)
<= ((k
- 1)
+ 1) by
XREAL_1: 7;
then p
< k by
NAT_1: 13;
then
A10: ((
free_magma_seq X)
. p)
=
{} by
A3;
A11: (fs
. p)
=
[:((
free_magma_seq X)
. p), ((
free_magma_seq X)
. (k
- p)):] by
A5,
A9
.=
{} by
A10,
ZFMISC_1: 90;
((
disjoin fs)
. p)
=
[:(fs
. p),
{p}:] by
A7,
CARD_3:def 3
.=
{} by
A11,
ZFMISC_1: 90;
hence y
c=
{} by
A6;
end;
then (
union (
rng (
disjoin fs)))
c=
{} by
ZFMISC_1: 76;
hence
P[k] by
A5,
CARD_3:def 4;
end;
end;
A12: for n be
Nat holds
P[n] from
NAT_1:sch 4(
A2);
for Y be
set st Y
in (
rng (
disjoin ((
free_magma_seq X)
|
NATPLUS ))) holds Y
c=
{}
proof
let Y be
set;
assume Y
in (
rng (
disjoin ((
free_magma_seq X)
|
NATPLUS )));
then
consider n be
object such that
A13: n
in (
dom (
disjoin ((
free_magma_seq X)
|
NATPLUS ))) & Y
= ((
disjoin ((
free_magma_seq X)
|
NATPLUS ))
. n) by
FUNCT_1:def 3;
A14: n
in (
dom ((
free_magma_seq X)
|
NATPLUS )) by
A13,
CARD_3:def 3;
then
reconsider n as
Nat;
A15: n
in (
dom ((
free_magma_seq X)
|
NATPLUS )) by
A13,
CARD_3:def 3;
((
disjoin ((
free_magma_seq X)
|
NATPLUS ))
. n)
=
[:(((
free_magma_seq X)
|
NATPLUS )
. n),
{n}:] by
A14,
CARD_3:def 3
.=
[:((
free_magma_seq X)
. n),
{n}:] by
A15,
FUNCT_1: 47
.=
[:
{} ,
{n}:] by
A12
.=
{} by
ZFMISC_1: 90;
hence Y
c=
{} by
A13;
end;
then (
union (
rng (
disjoin ((
free_magma_seq X)
|
NATPLUS ))))
c=
{} by
ZFMISC_1: 76;
hence (
free_magma_carrier X)
=
{} by
CARD_3:def 4;
end;
assume
A16: (
free_magma_carrier X)
=
{} ;
[:(
free_magma (X,1)),
{1}:]
c= (
free_magma_carrier X) by
Lm1;
hence X
=
{} by
A16;
end;
registration
let X be
empty
set;
cluster (
free_magma_carrier X) ->
empty;
correctness by
Th24;
end
registration
let X be non
empty
set;
cluster (
free_magma_carrier X) -> non
empty;
correctness by
Th24;
let w be
Element of (
free_magma_carrier X);
cluster (w
`2 ) -> non
zero
natural;
correctness
proof
w
in (
free_magma_carrier X);
then w
in (
union (
rng (
disjoin ((
free_magma_seq X)
|
NATPLUS )))) by
CARD_3:def 4;
then
consider Y be
set such that
A1: w
in Y & Y
in (
rng (
disjoin ((
free_magma_seq X)
|
NATPLUS ))) by
TARSKI:def 4;
consider n be
object such that
A2: n
in (
dom (
disjoin ((
free_magma_seq X)
|
NATPLUS ))) & Y
= ((
disjoin ((
free_magma_seq X)
|
NATPLUS ))
. n) by
A1,
FUNCT_1:def 3;
A3: n
in (
dom ((
free_magma_seq X)
|
NATPLUS )) by
A2,
CARD_3:def 3;
then n
in
NATPLUS by
RELAT_1: 57;
then
reconsider n as non
zero
Nat;
w
in
[:(((
free_magma_seq X)
|
NATPLUS )
. n),
{n}:] by
A2,
A1,
A3,
CARD_3:def 3;
then (w
`2 )
in
{n} by
MCART_1: 10;
hence thesis by
TARSKI:def 1;
end;
end
theorem ::
ALGSTR_4:25
Th25: for X be non
empty
set, w be
Element of (
free_magma_carrier X) holds w
in
[:(
free_magma (X,(w
`2 ))),
{(w
`2 )}:]
proof
let X be non
empty
set;
let w be
Element of (
free_magma_carrier X);
w
in (
free_magma_carrier X);
then w
in (
union (
rng (
disjoin ((
free_magma_seq X)
|
NATPLUS )))) by
CARD_3:def 4;
then
consider Y be
set such that
A1: w
in Y & Y
in (
rng (
disjoin ((
free_magma_seq X)
|
NATPLUS ))) by
TARSKI:def 4;
consider n be
object such that
A2: n
in (
dom (
disjoin ((
free_magma_seq X)
|
NATPLUS ))) & Y
= ((
disjoin ((
free_magma_seq X)
|
NATPLUS ))
. n) by
A1,
FUNCT_1:def 3;
A3: n
in (
dom ((
free_magma_seq X)
|
NATPLUS )) by
A2,
CARD_3:def 3;
then
A4: (((
free_magma_seq X)
|
NATPLUS )
. n)
= ((
free_magma_seq X)
. n) by
FUNCT_1: 47;
reconsider n as
Nat by
A3;
w
in
[:(((
free_magma_seq X)
|
NATPLUS )
. n),
{n}:] by
A2,
A1,
A3,
CARD_3:def 3;
then (w
`2 )
in
{n} by
MCART_1: 10;
then (w
`2 )
= n by
TARSKI:def 1;
hence w
in
[:(
free_magma (X,(w
`2 ))),
{(w
`2 )}:] by
A4,
A2,
A1,
A3,
CARD_3:def 3;
end;
theorem ::
ALGSTR_4:26
Th26: for X be non
empty
set, v,w be
Element of (
free_magma_carrier X) holds
[
[
[(v
`1 ), (w
`1 )], (v
`2 )], ((v
`2 )
+ (w
`2 ))] is
Element of (
free_magma_carrier X)
proof
let X be non
empty
set;
let v,w be
Element of (
free_magma_carrier X);
v
in
[:(
free_magma (X,(v
`2 ))),
{(v
`2 )}:] by
Th25;
then
A1: (v
`1 )
in (
free_magma (X,(v
`2 ))) by
MCART_1: 10;
w
in
[:(
free_magma (X,(w
`2 ))),
{(w
`2 )}:] by
Th25;
then (w
`1 )
in (
free_magma (X,(w
`2 ))) by
MCART_1: 10;
then
A2:
[
[(v
`1 ), (w
`1 )], (v
`2 )]
in (
free_magma (X,((v
`2 )
+ (w
`2 )))) by
A1,
Th22;
A3: ((v
`2 )
+ (w
`2 ))
in
{((v
`2 )
+ (w
`2 ))} by
TARSKI:def 1;
set z =
[
[
[(v
`1 ), (w
`1 )], (v
`2 )], ((v
`2 )
+ (w
`2 ))];
A4: (z
`1 )
in (
free_magma (X,((v
`2 )
+ (w
`2 )))) by
A2;
(z
`2 )
in
{((v
`2 )
+ (w
`2 ))} by
A3;
then
A5: z
in
[:(
free_magma (X,((v
`2 )
+ (w
`2 )))),
{((v
`2 )
+ (w
`2 ))}:] by
A4,
ZFMISC_1:def 2;
[:(
free_magma (X,((v
`2 )
+ (w
`2 )))),
{((v
`2 )
+ (w
`2 ))}:]
c= (
free_magma_carrier X) by
Lm1;
hence thesis by
A5;
end;
theorem ::
ALGSTR_4:27
Th27: X
c= Y implies (
free_magma_carrier X)
c= (
free_magma_carrier Y)
proof
assume
A1: X
c= Y;
per cases ;
suppose X
=
{} ;
then (
free_magma_carrier X)
=
{} ;
hence (
free_magma_carrier X)
c= (
free_magma_carrier Y);
end;
suppose
A2: X
<>
{} ;
let x be
object;
assume
A3: x
in (
free_magma_carrier X);
reconsider X9 = X as non
empty
set by
A2;
reconsider w = x as
Element of (
free_magma_carrier X9) by
A3;
A4: w
in
[:(
free_magma (X9,(w
`2 ))),
{(w
`2 )}:] by
Th25;
then
A5: (w
`1 )
in (
free_magma (X9,(w
`2 ))) & (w
`2 )
in
{(w
`2 )} by
MCART_1: 10;
reconsider Y9 = Y as non
empty
set by
A2,
A1;
A6: (
free_magma (X9,(w
`2 )))
c= (
free_magma (Y9,(w
`2 ))) by
A1,
Th23;
w
=
[(w
`1 ), (w
`2 )] by
A4,
MCART_1: 21;
then
A7: w
in
[:(
free_magma (Y9,(w
`2 ))),
{(w
`2 )}:] by
A6,
A5,
ZFMISC_1:def 2;
[:(
free_magma (Y9,(w
`2 ))),
{(w
`2 )}:]
c= (
free_magma_carrier Y9) by
Lm1;
hence x
in (
free_magma_carrier Y) by
A7;
end;
end;
theorem ::
ALGSTR_4:28
n
>
0 implies
[:(
free_magma (X,n)),
{n}:]
c= (
free_magma_carrier X) by
Lm1;
definition
let X be
set;
::
ALGSTR_4:def16
func
free_magma_mult X ->
BinOp of (
free_magma_carrier X) means
:
Def16: for v,w be
Element of (
free_magma_carrier X), n, m st n
= (v
`2 ) & m
= (w
`2 ) holds (it
. (v,w))
=
[
[
[(v
`1 ), (w
`1 )], (v
`2 )], (n
+ m)] if X is non
empty
otherwise it
=
{} ;
correctness
proof
A1: X is non
empty implies ex f be
BinOp of (
free_magma_carrier X) st for v,w be
Element of (
free_magma_carrier X), n, m st n
= (v
`2 ) & m
= (w
`2 ) holds (f
. (v,w))
=
[
[
[(v
`1 ), (w
`1 )], (v
`2 )], (n
+ m)]
proof
assume
A2: X is non
empty;
defpred
P[
set,
set,
set] means for n, m st n
= ($1
`2 ) & m
= ($2
`2 ) holds $3
=
[
[
[($1
`1 ), ($2
`1 )], ($1
`2 )], (n
+ m)];
reconsider Y = (
free_magma_carrier X) as non
empty
set by
A2;
A3: for x be
Element of Y holds for y be
Element of Y holds ex z be
Element of Y st
P[x, y, z]
proof
let x be
Element of Y;
let y be
Element of Y;
reconsider X9 = X as non
empty
set by
A2;
reconsider v = x as
Element of (
free_magma_carrier X9);
reconsider w = y as
Element of (
free_magma_carrier X9);
reconsider z =
[
[
[(v
`1 ), (w
`1 )], (v
`2 )], ((v
`2 )
+ (w
`2 ))] as
Element of Y by
Th26;
take z;
thus thesis;
end;
consider f be
Function of
[:Y, Y:], Y such that
A4: for x be
Element of Y holds for y be
Element of Y holds
P[x, y, (f
. (x,y))] from
BINOP_1:sch 3(
A3);
reconsider f as
BinOp of (
free_magma_carrier X);
take f;
thus thesis by
A4;
end;
A5: X is
empty implies ex f be
BinOp of (
free_magma_carrier X) st f
=
{}
proof
assume
A6: X is
empty;
then
A7: (
free_magma_carrier X)
=
{} ;
{}
c=
[:
{} qua
set,
{} qua
set:];
then
reconsider f =
{} as
Relation of
[:
{} qua
set,
{} qua
set:],
{} by
ZFMISC_1: 90;
(
[:
{} qua
set,
{} qua
set:]
=
{} implies
{}
=
{} ) & (
dom f)
=
[:
{} qua
set,
{} qua
set:] by
ZFMISC_1: 90;
then
reconsider f =
{} as
BinOp of
{} by
FUNCT_2:def 1;
for v,w be
Element of (
free_magma_carrier X), n, m st n
= (v
`2 ) & m
= (w
`2 ) & v
in (
free_magma_carrier X) & w
in (
free_magma_carrier X) holds (f
. (v,w))
=
[
[
[(v
`1 ), (w
`1 )], (v
`2 )], (n
+ m)] by
A6;
hence thesis by
A7;
end;
now
let f1,f2 be
BinOp of (
free_magma_carrier X);
thus X is non
empty & (for v,w be
Element of (
free_magma_carrier X), n, m st n
= (v
`2 ) & m
= (w
`2 ) holds (f1
. (v,w))
=
[
[
[(v
`1 ), (w
`1 )], (v
`2 )], (n
+ m)]) & (for v,w be
Element of (
free_magma_carrier X), n, m st n
= (v
`2 ) & m
= (w
`2 ) holds (f2
. (v,w))
=
[
[
[(v
`1 ), (w
`1 )], (v
`2 )], (n
+ m)]) implies f1
= f2
proof
assume
A8: X is non
empty;
assume
A9: for v,w be
Element of (
free_magma_carrier X), n, m st n
= (v
`2 ) & m
= (w
`2 ) holds (f1
. (v,w))
=
[
[
[(v
`1 ), (w
`1 )], (v
`2 )], (n
+ m)];
assume
A10: for v,w be
Element of (
free_magma_carrier X), n, m st n
= (v
`2 ) & m
= (w
`2 ) holds (f2
. (v,w))
=
[
[
[(v
`1 ), (w
`1 )], (v
`2 )], (n
+ m)];
for v,w be
Element of (
free_magma_carrier X) holds (f1
. (v,w))
= (f2
. (v,w))
proof
let v,w be
Element of (
free_magma_carrier X);
set n = (v
`2 ), m = (w
`2 );
reconsider n, m as
Nat by
A8;
thus (f1
. (v,w))
=
[
[
[(v
`1 ), (w
`1 )], (v
`2 )], (n
+ m)] by
A9
.= (f2
. (v,w)) by
A10;
end;
hence f1
= f2 by
BINOP_1: 2;
end;
assume X is
empty & f1
=
{} & f2
=
{} ;
hence thesis;
end;
hence thesis by
A1,
A5;
end;
end
definition
let X be
set;
::
ALGSTR_4:def17
func
free_magma X ->
multMagma equals
multMagma (# (
free_magma_carrier X), (
free_magma_mult X) #);
correctness ;
end
registration
let X be
set;
cluster (
free_magma X) ->
strict;
correctness ;
end
registration
let X be
empty
set;
cluster (
free_magma X) ->
empty;
correctness ;
end
registration
let X be non
empty
set;
cluster (
free_magma X) -> non
empty;
correctness ;
let w be
Element of (
free_magma X);
cluster (w
`2 ) -> non
zero
natural;
correctness ;
end
theorem ::
ALGSTR_4:29
for X be
set, S be
Subset of X holds (
free_magma S) is
multSubmagma of (
free_magma X)
proof
let X be
set;
let S be
Subset of X;
A1: the
carrier of (
free_magma S)
c= the
carrier of (
free_magma X) by
Th27;
reconsider A = the
carrier of (
free_magma S) as
set;
A2: (the
multF of (
free_magma X)
|
[:A, A:])
= (the
multF of (
free_magma X)
|| the
carrier of (
free_magma S)) by
REALSET1:def 2;
per cases ;
suppose
A3: S is
empty;
then
A4: the
carrier of (
free_magma S)
=
{} ;
the
multF of (
free_magma S)
= (the
multF of (
free_magma X)
|
{} ) by
A3
.= (the
multF of (
free_magma X)
|
[:A, A:]) by
A4,
ZFMISC_1: 90;
hence thesis by
A2,
A1,
Def9;
end;
suppose
A5: not S is
empty;
then
A6: (
dom the
multF of (
free_magma S))
=
[:A, A:] by
FUNCT_2:def 1;
A7: X is non
empty by
A5;
[:A, A:]
c=
[:(
free_magma_carrier X), (
free_magma_carrier X):] by
A1,
ZFMISC_1: 96;
then
[:A, A:]
c= (
dom the
multF of (
free_magma X)) by
A7,
FUNCT_2:def 1;
then
A8: (
dom the
multF of (
free_magma S))
= (
dom (the
multF of (
free_magma X)
|| the
carrier of (
free_magma S))) by
A6,
A2,
RELAT_1: 62;
for z be
object st z
in (
dom the
multF of (
free_magma S)) holds (the
multF of (
free_magma S)
. z)
= ((the
multF of (
free_magma X)
|| the
carrier of (
free_magma S))
. z)
proof
let z be
object;
assume
A9: z
in (
dom the
multF of (
free_magma S));
then
consider x,y be
object such that
A10: x
in A & y
in A & z
=
[x, y] by
ZFMISC_1:def 2;
reconsider x, y as
Element of (
free_magma_carrier S) by
A10;
reconsider n = (x
`2 ), m = (y
`2 ) as
Nat by
A5;
reconsider x9 = x, y9 = y as
Element of (
free_magma_carrier X) by
A10,
A1;
(the
multF of (
free_magma S)
. z)
= (the
multF of (
free_magma S)
. (x,y)) by
A10,
BINOP_1:def 1
.=
[
[
[(x
`1 ), (y
`1 )], (x
`2 )], (n
+ m)] by
A5,
Def16
.= ((
free_magma_mult X)
. (x9,y9)) by
A7,
Def16
.= (the
multF of (
free_magma X)
. z) by
A10,
BINOP_1:def 1
.= ((the
multF of (
free_magma X)
|
[:A, A:])
. z) by
A9,
FUNCT_1: 49;
hence thesis by
REALSET1:def 2;
end;
then the
multF of (
free_magma S)
= (the
multF of (
free_magma X)
|| the
carrier of (
free_magma S)) by
A8,
FUNCT_1: 2;
hence (
free_magma S) is
multSubmagma of (
free_magma X) by
A1,
Def9;
end;
end;
definition
let X be
set;
let w be
Element of (
free_magma X);
::
ALGSTR_4:def18
func
length w ->
Nat equals
:
Def18: (w
`2 ) if X is non
empty
otherwise
0 ;
correctness ;
end
theorem ::
ALGSTR_4:30
Th30: X
= { (w
`1 ) where w be
Element of (
free_magma X) : (
length w)
= 1 }
proof
for x be
object holds x
in X iff x
in { (w
`1 ) where w be
Element of (
free_magma X) : (
length w)
= 1 }
proof
let x be
object;
hereby
assume
A1: x
in X;
then
A2: x
in (
free_magma (X,1)) by
Def13;
1
in
{1} by
TARSKI:def 1;
then
A3:
[x, 1]
in
[:(
free_magma (X,1)),
{1}:] by
A2,
ZFMISC_1:def 2;
[:(
free_magma (X,1)),
{1}:]
c= (
free_magma_carrier X) by
Lm1;
then
reconsider w9 =
[x, 1] as
Element of (
free_magma X) by
A3;
1
= (
[x, 1]
`2 );
then
A4: (
length w9)
= 1 by
A1,
Def18;
x
= (
[x, 1]
`1 );
hence x
in { (w
`1 ) where w be
Element of (
free_magma X) : (
length w)
= 1 } by
A4;
end;
assume x
in { (w
`1 ) where w be
Element of (
free_magma X) : (
length w)
= 1 };
then
consider w be
Element of (
free_magma X) such that
A5: x
= (w
`1 ) & (
length w)
= 1;
A6: (w
`2 )
= 1 by
A5,
Def18;
per cases ;
suppose X is non
empty;
then w
in
[:(
free_magma (X,1)),
{1}:] by
A6,
Th25;
then w
in
[:X,
{1}:] by
Def13;
hence x
in X by
A5,
MCART_1: 10;
end;
suppose X is
empty;
hence thesis by
A5,
Def18;
end;
end;
hence thesis by
TARSKI: 2;
end;
reserve v,v1,v2,w,w1,w2 for
Element of (
free_magma X);
theorem ::
ALGSTR_4:31
Th31: X is non
empty implies (v
* w)
=
[
[
[(v
`1 ), (w
`1 )], (v
`2 )], ((
length v)
+ (
length w))]
proof
assume
A1: X is non
empty;
then (
length v)
= (v
`2 ) & (
length w)
= (w
`2 ) by
Def18;
hence thesis by
A1,
Def16;
end;
theorem ::
ALGSTR_4:32
Th32: X is non
empty implies v
=
[(v
`1 ), (v
`2 )] & (
length v)
>= 1
proof
assume X is non
empty;
then
reconsider X9 = X as non
empty
set;
reconsider v9 = v as
Element of (
free_magma X9);
v9
in
[:(
free_magma (X,(v9
`2 ))),
{(v9
`2 )}:] by
Th25;
then ex x,y be
object st x
in (
free_magma (X,(v9
`2 ))) & y
in
{(v9
`2 )} & v9
=
[x, y] by
ZFMISC_1:def 2;
hence v
=
[(v
`1 ), (v
`2 )];
reconsider v99 = v9 as
Element of (
free_magma_carrier X9);
(v99
`2 )
>
0 ;
then (
length v9)
>
0 by
Def18;
then ((
length v9)
+ 1)
> (
0
+ 1) by
XREAL_1: 6;
hence thesis by
NAT_1: 13;
end;
theorem ::
ALGSTR_4:33
(
length (v
* w))
= ((
length v)
+ (
length w))
proof
set vw = (v
* w);
per cases ;
suppose
A1: X is non
empty;
then (v
* w)
=
[
[
[(v
`1 ), (w
`1 )], (v
`2 )], ((
length v)
+ (
length w))] by
Th31;
hence (
length (v
* w))
= (
[
[
[(v
`1 ), (w
`1 )], (v
`2 )], ((
length v)
+ (
length w))]
`2 ) by
A1,
Def18
.= ((
length v)
+ (
length w));
end;
suppose
A2: X is
empty;
hence (
length (v
* w))
=
0 by
Def18
.= ((
length v)
+
0 ) by
A2,
Def18
.= ((
length v)
+ (
length w)) by
A2,
Def18;
end;
end;
theorem ::
ALGSTR_4:34
Th34: (
length w)
>= 2 implies ex w1, w2 st w
= (w1
* w2) & (
length w1)
< (
length w) & (
length w2)
< (
length w)
proof
assume
A1: (
length w)
>= 2;
then
reconsider X9 = X as non
empty
set by
Def18;
reconsider w9 = w as
Element of (
free_magma X9);
A2: w9
in
[:(
free_magma (X,(w9
`2 ))),
{(w9
`2 )}:] by
Th25;
set n = (
length w);
A3: n
= (w9
`2 ) by
Def18;
consider fs be
FinSequence such that
A4: (
len fs)
= (n
- 1) and
A5: (for p be
Nat st p
>= 1 & p
<= (n
- 1) holds (fs
. p)
=
[:((
free_magma_seq X)
. p), ((
free_magma_seq X)
. (n
- p)):]) and
A6: ((
free_magma_seq X)
. n)
= (
Union (
disjoin fs)) by
A1,
Def13;
(w9
`1 )
in ((
free_magma_seq X)
. n) by
A3,
A2,
MCART_1: 10;
then (w9
`1 )
in (
union (
rng (
disjoin fs))) by
A6,
CARD_3:def 4;
then
consider Y be
set such that
A7: (w9
`1 )
in Y & Y
in (
rng (
disjoin fs)) by
TARSKI:def 4;
consider p be
object such that
A8: p
in (
dom (
disjoin fs)) & Y
= ((
disjoin fs)
. p) by
A7,
FUNCT_1:def 3;
A9: p
in (
dom fs) by
A8,
CARD_3:def 3;
then
reconsider p as
Nat;
A10: p
in (
Seg (
len fs)) by
A9,
FINSEQ_1:def 3;
then
A11: 1
<= p & p
<= (
len fs) by
FINSEQ_1: 1;
then (fs
. p)
=
[:((
free_magma_seq X)
. p), ((
free_magma_seq X)
. (n
- p)):] by
A4,
A5;
then
A12: (w9
`1 )
in
[:
[:((
free_magma_seq X)
. p), ((
free_magma_seq X)
. (n
- p)):],
{p}:] by
A7,
A8,
A9,
CARD_3:def 3;
then
A13: ((w9
`1 )
`1 )
in
[:((
free_magma_seq X)
. p), ((
free_magma_seq X)
. (n
- p)):] & ((w9
`1 )
`2 )
in
{p} by
MCART_1: 10;
then
A14: (((w9
`1 )
`1 )
`1 )
in ((
free_magma_seq X)
. p) & (((w9
`1 )
`1 )
`2 )
in ((
free_magma_seq X)
. (n
- p)) by
MCART_1: 10;
(
- p)
>= (
- (n
- 1)) by
A11,
A4,
XREAL_1: 24;
then
A15: ((
- p)
+ n)
>= ((
- (n
- 1))
+ n) by
XREAL_1: 7;
then (n
- p)
in
NAT by
INT_1: 3;
then
reconsider m = (n
- p) as
Nat;
set w19 =
[(((w9
`1 )
`1 )
`1 ), p];
set w29 =
[(((w9
`1 )
`1 )
`2 ), m];
p
in
{p} by
TARSKI:def 1;
then
A16: w19
in
[:(
free_magma (X,p)),
{p}:] by
A14,
ZFMISC_1:def 2;
m
in
{m} by
TARSKI:def 1;
then
A17: w29
in
[:(
free_magma (X,m)),
{m}:] by
A14,
ZFMISC_1:def 2;
[:(
free_magma (X,p)),
{p}:]
c= (
free_magma_carrier X) by
A11,
Lm1;
then
reconsider w19 as
Element of (
free_magma_carrier X) by
A16;
[:(
free_magma (X,m)),
{m}:]
c= (
free_magma_carrier X) by
A15,
Lm1;
then
reconsider w29 as
Element of (
free_magma_carrier X) by
A17;
reconsider w1 = w19, w2 = w29 as
Element of (
free_magma X);
A18: (
length w1)
= (
[(((w9
`1 )
`1 )
`1 ), p]
`2 ) by
Def18
.= p;
A19: (
length w2)
= (
[(((w9
`1 )
`1 )
`2 ), m]
`2 ) by
Def18
.= m;
ex x,y be
object st x
in
[:((
free_magma_seq X)
. p), ((
free_magma_seq X)
. (n
- p)):] & y
in
{p} & (w9
`1 )
=
[x, y] by
A12,
ZFMISC_1:def 2;
then
A20: (w9
`1 )
=
[((w9
`1 )
`1 ), ((w9
`1 )
`2 )]
.=
[((w9
`1 )
`1 ), p] by
A13,
TARSKI:def 1;
A21: ex x,y be
object st x
in ((
free_magma_seq X)
. p) & y
in ((
free_magma_seq X)
. (n
- p)) & ((w9
`1 )
`1 )
=
[x, y] by
A13,
ZFMISC_1:def 2;
take w1, w2;
ex x,y be
object st x
in (
free_magma (X,(w9
`2 ))) & y
in
{(w9
`2 )} & w9
=
[x, y] by
A2,
ZFMISC_1:def 2;
hence w
=
[(w9
`1 ), (w9
`2 )]
.=
[
[((w9
`1 )
`1 ), p], n] by
A20,
Def18
.=
[
[((w9
`1 )
`1 ), (w1
`2 )], ((
length w1)
+ (
length w2))] by
A18,
A19
.=
[
[
[(((w9
`1 )
`1 )
`1 ), (((w9
`1 )
`1 )
`2 )], (w1
`2 )], ((
length w1)
+ (
length w2))] by
A21
.=
[
[
[(((w9
`1 )
`1 )
`1 ), (w2
`1 )], (w1
`2 )], ((
length w1)
+ (
length w2))]
.=
[
[
[(w1
`1 ), (w2
`1 )], (w1
`2 )], ((
length w1)
+ (
length w2))]
.= (w1
* w2) by
Th31;
p
<= (n
- 1) by
A10,
A4,
FINSEQ_1: 1;
then (p
+ 1)
<= ((n
- 1)
+ 1) by
XREAL_1: 7;
hence (
length w1)
< (
length w) by
A18,
NAT_1: 13;
(
- 1)
>= (
- p) by
A11,
XREAL_1: 24;
then ((
- 1)
+ (n
+ 1))
>= ((
- p)
+ (n
+ 1)) by
XREAL_1: 7;
then n
>= (m
+ 1);
hence (
length w2)
< (
length w) by
A19,
NAT_1: 13;
end;
theorem ::
ALGSTR_4:35
(v1
* v2)
= (w1
* w2) implies v1
= w1 & v2
= w2
proof
assume
A1: (v1
* v2)
= (w1
* w2);
per cases ;
suppose
A2: X is non
empty;
then (v1
* v2)
=
[
[
[(v1
`1 ), (v2
`1 )], (v1
`2 )], ((
length v1)
+ (
length v2))] & (w1
* w2)
=
[
[
[(w1
`1 ), (w2
`1 )], (w1
`2 )], ((
length w1)
+ (
length w2))] by
Th31;
then
A3:
[
[(v1
`1 ), (v2
`1 )], (v1
`2 )]
=
[
[(w1
`1 ), (w2
`1 )], (w1
`2 )] & ((
length v1)
+ (
length v2))
= ((
length w1)
+ (
length w2)) by
A1,
XTUPLE_0: 1;
then
A4:
[(v1
`1 ), (v2
`1 )]
=
[(w1
`1 ), (w2
`1 )] & (v1
`2 )
= (w1
`2 ) by
XTUPLE_0: 1;
(
length v1)
= (v1
`2 ) by
A2,
Def18
.= (
length w1) by
A2,
A4,
Def18;
then (v2
`2 )
= (
length w2) by
A2,
A3,
Def18;
then
A5: (v2
`2 )
= (w2
`2 ) by
A2,
Def18;
thus v1
=
[(v1
`1 ), (v1
`2 )] by
A2,
Th32
.=
[(w1
`1 ), (w1
`2 )] by
A4,
XTUPLE_0: 1
.= w1 by
A2,
Th32;
thus v2
=
[(v2
`1 ), (v2
`2 )] by
A2,
Th32
.=
[(w2
`1 ), (w2
`2 )] by
A5,
A4,
XTUPLE_0: 1
.= w2 by
A2,
Th32;
end;
suppose X is
empty;
then v1
=
{} & w1
=
{} & v2
=
{} & w2
=
{} by
SUBSET_1:def 1;
hence thesis;
end;
end;
definition
let X be
set;
let n be
Nat;
::
ALGSTR_4:def19
func
canon_image (X,n) ->
Function of (
free_magma (X,n)), (
free_magma X) means
:
Def19: for x st x
in (
dom it ) holds (it
. x)
=
[x, n] if n
>
0
otherwise it
=
{} ;
correctness
proof
A1: n
>
0 implies ex f be
Function of (
free_magma (X,n)), (
free_magma X) st for x st x
in (
dom f) holds (f
. x)
=
[x, n]
proof
assume
A2: n
>
0 ;
deffunc
F(
object) =
[$1, n];
A3: for x be
object st x
in (
free_magma (X,n)) holds
F(x)
in the
carrier of (
free_magma X)
proof
let x be
object;
assume
A4: x
in (
free_magma (X,n));
n
in
{n} by
TARSKI:def 1;
then
A5:
F(x)
in
[:(
free_magma (X,n)),
{n}:] by
A4,
ZFMISC_1:def 2;
[:(
free_magma (X,n)),
{n}:]
c= (
free_magma_carrier X) by
A2,
Lm1;
hence
F(x)
in the
carrier of (
free_magma X) by
A5;
end;
consider f be
Function of (
free_magma (X,n)), the
carrier of (
free_magma X) such that
A6: for x be
object st x
in (
free_magma (X,n)) holds (f
. x)
=
F(x) from
FUNCT_2:sch 2(
A3);
take f;
let x;
assume x
in (
dom f);
hence (f
. x)
=
[x, n] by
A6;
end;
A7: not n
>
0 implies ex f be
Function of (
free_magma (X,n)), (
free_magma X) st f
=
{}
proof
assume not n
>
0 ;
then n
=
0 ;
then
A8: (
free_magma (X,n))
=
{} by
Def13;
set f =
{} ;
A9: (
dom f)
=
{} ;
(
rng f)
c= the
carrier of (
free_magma X);
then
reconsider f as
Function of (
free_magma (X,n)), (
free_magma X) by
A8,
A9,
FUNCT_2: 2;
take f;
thus f
=
{} ;
end;
for f1,f2 be
Function of (
free_magma (X,n)), (
free_magma X) holds n
>
0 & (for x st x
in (
dom f1) holds (f1
. x)
=
[x, n]) & (for x st x
in (
dom f2) holds (f2
. x)
=
[x, n]) implies f1
= f2
proof
let f1,f2 be
Function of (
free_magma (X,n)), (
free_magma X);
assume n
>
0 ;
assume
A10: for x st x
in (
dom f1) holds (f1
. x)
=
[x, n];
assume
A11: for x st x
in (
dom f2) holds (f2
. x)
=
[x, n];
per cases ;
suppose X is
empty;
hence thesis;
end;
suppose
A12: X is non
empty;
then
A13: (
dom f1)
= (
free_magma (X,n)) by
FUNCT_2:def 1
.= (
dom f2) by
A12,
FUNCT_2:def 1;
for x be
object st x
in (
dom f1) holds (f1
. x)
= (f2
. x)
proof
let x be
object;
assume
A14: x
in (
dom f1);
hence (f1
. x)
=
[x, n] by
A10
.= (f2
. x) by
A11,
A13,
A14;
end;
hence thesis by
A13,
FUNCT_1: 2;
end;
end;
hence thesis by
A1,
A7;
end;
end
Lm2: (
canon_image (X,n)) is
one-to-one
proof
for x1,x2 be
object st x1
in (
dom (
canon_image (X,n))) & x2
in (
dom (
canon_image (X,n))) & ((
canon_image (X,n))
. x1)
= ((
canon_image (X,n))
. x2) holds x1
= x2
proof
let x1,x2 be
object;
assume
A1: x1
in (
dom (
canon_image (X,n))) & x2
in (
dom (
canon_image (X,n)));
assume
A2: ((
canon_image (X,n))
. x1)
= ((
canon_image (X,n))
. x2);
per cases ;
suppose n
>
0 ;
then ((
canon_image (X,n))
. x1)
=
[x1, n] & ((
canon_image (X,n))
. x2)
=
[x2, n] by
A1,
Def19;
hence x1
= x2 by
A2,
XTUPLE_0: 1;
end;
suppose not n
>
0 ;
then (
canon_image (X,n))
=
{} by
Def19;
hence thesis by
A1;
end;
end;
hence (
canon_image (X,n)) is
one-to-one by
FUNCT_1:def 4;
end;
registration
let X be
set;
let n be
Nat;
cluster (
canon_image (X,n)) ->
one-to-one;
correctness by
Lm2;
end
reserve X,Y,Z for non
empty
set;
Lm3: (
dom (
canon_image (X,1)))
= X & for x be
set st x
in X holds ((
canon_image (X,1))
. x)
=
[x, 1]
proof
(
dom (
canon_image (X,1)))
= (
free_magma (X,1)) by
FUNCT_2:def 1;
hence (
dom (
canon_image (X,1)))
= X by
Def13;
hence for x be
set st x
in X holds ((
canon_image (X,1))
. x)
=
[x, 1] by
Def19;
end;
theorem ::
ALGSTR_4:36
Th36: for A be
Subset of (
free_magma X) st A
= ((
canon_image (X,1))
.: X) holds (
free_magma X)
= (
the_submagma_generated_by A)
proof
let A be
Subset of (
free_magma X);
set N = (
the_submagma_generated_by A);
assume
A1: A
= ((
canon_image (X,1))
.: X);
per cases ;
suppose
A2: A is
empty;
X is
empty
proof
assume X is non
empty;
consider x be
object such that
A3: x
in X by
XBOOLE_0:def 1;
x
in (
dom (
canon_image (X,1))) by
Lm3,
A3;
then ((
canon_image (X,1))
. x)
in ((
canon_image (X,1))
.: X) by
A3,
FUNCT_1:def 6;
hence contradiction by
A2,
A1;
end;
hence thesis;
end;
suppose
A4: not A is
empty;
A5: the
carrier of N
c= the
carrier of (
free_magma X) by
Def9;
for x be
object st x
in the
carrier of (
free_magma X) holds x
in the
carrier of N
proof
let x be
object;
assume
A6: x
in the
carrier of (
free_magma X);
defpred
P[
Nat] means for v be
Element of (
free_magma X) st (
length v)
= $1 holds v
in the
carrier of N;
A7: for k be
Nat st for n be
Nat st n
< k holds
P[n] holds
P[k]
proof
let k be
Nat;
assume
A8: for n be
Nat st n
< k holds
P[n];
k
=
0 or (k
+ 1)
> (
0
+ 1) by
XREAL_1: 6;
then k
=
0 or k
>= 1 by
NAT_1: 13;
then k
=
0 or k
= 1 or k
> 1 by
XXREAL_0: 1;
then
A9: k
=
0 or k
= 1 or (k
+ 1)
> (1
+ 1) by
XREAL_1: 6;
per cases by
A9,
NAT_1: 13;
suppose k
=
0 ;
hence
P[k] by
Th32;
end;
suppose
A10: k
= 1;
for v be
Element of (
free_magma X) st (
length v)
= 1 holds v
in the
carrier of N
proof
let v be
Element of (
free_magma X);
assume
A11: (
length v)
= 1;
A12: v
=
[(v
`1 ), (v
`2 )] by
Th32
.=
[(v
`1 ), 1] by
A11,
Def18;
(v
`1 )
in { (w
`1 ) where w be
Element of (
free_magma X) : (
length w)
= 1 } by
A11;
then (v
`1 )
in X by
Th30;
then (v
`1 )
in (
dom (
canon_image (X,1))) & (v
`1 )
in X & v
= ((
canon_image (X,1))
. (v
`1 )) by
A12,
Lm3;
then
A13: v
in A by
A1,
FUNCT_1:def 6;
A
c= the
carrier of N by
Def12;
hence thesis by
A13;
end;
hence
P[k] by
A10;
end;
suppose
A14: k
>= 2;
for v be
Element of (
free_magma X) st (
length v)
= k holds v
in the
carrier of N
proof
let v be
Element of (
free_magma X);
assume
A15: (
length v)
= k;
then
consider v1,v2 be
Element of (
free_magma X) such that
A16: v
= (v1
* v2) & (
length v1)
< (
length v) & (
length v2)
< (
length v) by
A14,
Th34;
A17: v1
in the
carrier of N by
A8,
A15,
A16;
reconsider v19 = v1 as
Element of N by
A8,
A15,
A16;
A18: v2
in the
carrier of N by
A8,
A15,
A16;
reconsider v29 = v2 as
Element of N by
A8,
A15,
A16;
N is non
empty by
A4,
Th14;
then
A19: the
carrier of N
<>
{} ;
A20:
[v1, v2]
in
[:the
carrier of N, the
carrier of N:] by
A17,
A18,
ZFMISC_1: 87;
(v19
* v29)
= (the
multF of N
.
[v19, v29]) by
BINOP_1:def 1
.= ((the
multF of (
free_magma X)
|| the
carrier of N)
.
[v1, v2]) by
Def9
.= ((the
multF of (
free_magma X)
|
[:the
carrier of N, the
carrier of N:])
.
[v1, v2]) by
REALSET1:def 2
.= (the
multF of (
free_magma X)
.
[v1, v2]) by
A20,
FUNCT_1: 49
.= (v1
* v2) by
BINOP_1:def 1;
hence v
in the
carrier of N by
A16,
A19;
end;
hence
P[k];
end;
end;
A21: for n be
Nat holds
P[n] from
NAT_1:sch 4(
A7);
reconsider v = x as
Element of (
free_magma X) by
A6;
reconsider k = (
length v) as
Nat;
P[k] by
A21;
hence x
in the
carrier of N;
end;
then the
carrier of (
free_magma X)
c= the
carrier of N;
then the
carrier of (
free_magma X)
= the
carrier of N by
A5,
XBOOLE_0:def 10;
hence thesis by
Th7;
end;
end;
theorem ::
ALGSTR_4:37
for R be
compatible
Equivalence_Relation of (
free_magma X) holds ((
free_magma X)
./. R)
= (
the_submagma_generated_by ((
nat_hom R)
.: ((
canon_image (X,1))
.: X)))
proof
let R be
compatible
Equivalence_Relation of (
free_magma X);
set A = ((
canon_image (X,1))
.: X);
reconsider A as
Subset of (
free_magma X);
A1: the
carrier of (
the_submagma_generated_by A)
= the
carrier of (
free_magma X) by
Th36;
the
carrier of ((
free_magma X)
./. R)
= (
rng (
nat_hom R)) by
FUNCT_2:def 3;
then the
carrier of ((
free_magma X)
./. R)
= ((
nat_hom R)
.: (
dom (
nat_hom R))) by
RELAT_1: 113;
then the
carrier of ((
free_magma X)
./. R)
= ((
nat_hom R)
.: the
carrier of (
the_submagma_generated_by A)) by
A1,
FUNCT_2:def 1;
then the
carrier of ((
free_magma X)
./. R)
= the
carrier of (
the_submagma_generated_by ((
nat_hom R)
.: A)) by
Th15;
hence thesis by
Th7;
end;
theorem ::
ALGSTR_4:38
Th38: for f be
Function of X, Y holds ((
canon_image (Y,1))
* f) is
Function of X, (
free_magma Y)
proof
let f be
Function of X, Y;
A1: (
dom f)
= X by
FUNCT_2:def 1;
(
dom (
canon_image (Y,1)))
= Y by
Lm3;
then (
rng f)
c= (
dom (
canon_image (Y,1)));
then
A2: (
dom ((
canon_image (Y,1))
* f))
= X by
A1,
RELAT_1: 27;
(
rng ((
canon_image (Y,1))
* f))
c= (
rng (
canon_image (Y,1))) by
RELAT_1: 26;
hence thesis by
A2,
FUNCT_2: 2;
end;
definition
let X be non
empty
set;
let M be non
empty
multMagma;
let n,m be non
zero
Nat;
let f be
Function of (
free_magma (X,n)), M;
let g be
Function of (
free_magma (X,m)), M;
::
ALGSTR_4:def20
func
[:f,g:] ->
Function of
[:
[:(
free_magma (X,n)), (
free_magma (X,m)):],
{n}:], M means
:
Def20: for x be
Element of
[:
[:(
free_magma (X,n)), (
free_magma (X,m)):],
{n}:], y be
Element of (
free_magma (X,n)), z be
Element of (
free_magma (X,m)) st y
= ((x
`1 )
`1 ) & z
= ((x
`1 )
`2 ) holds (it
. x)
= ((f
. y)
* (g
. z));
existence
proof
set X1 =
[:
[:(
free_magma (X,n)), (
free_magma (X,m)):],
{n}:];
defpred
P[
object,
object] means for x be
Element of X1, y be
Element of (
free_magma (X,n)), z be
Element of (
free_magma (X,m)) st $1
= x & y
= ((x
`1 )
`1 ) & z
= ((x
`1 )
`2 ) holds $2
= ((f
. y)
* (g
. z));
A1: for x be
object st x
in X1 holds ex y be
object st y
in the
carrier of M &
P[x, y]
proof
let x be
object;
assume x
in X1;
then
A2: (x
`1 )
in
[:(
free_magma (X,n)), (
free_magma (X,m)):] by
MCART_1: 10;
then
reconsider x1 = ((x
`1 )
`1 ) as
Element of (
free_magma (X,n)) by
MCART_1: 10;
reconsider x2 = ((x
`1 )
`2 ) as
Element of (
free_magma (X,m)) by
A2,
MCART_1: 10;
set y = ((f
. x1)
* (g
. x2));
take y;
thus y
in the
carrier of M;
thus
P[x, y];
end;
consider h be
Function of X1, the
carrier of M such that
A3: for x be
object st x
in X1 holds
P[x, (h
. x)] from
FUNCT_2:sch 1(
A1);
take h;
thus thesis by
A3;
end;
uniqueness
proof
let f1,f2 be
Function of
[:
[:(
free_magma (X,n)), (
free_magma (X,m)):],
{n}:], M;
assume
A4: for x be
Element of
[:
[:(
free_magma (X,n)), (
free_magma (X,m)):],
{n}:], y be
Element of (
free_magma (X,n)), z be
Element of (
free_magma (X,m)) st y
= ((x
`1 )
`1 ) & z
= ((x
`1 )
`2 ) holds (f1
. x)
= ((f
. y)
* (g
. z));
assume
A5: for x be
Element of
[:
[:(
free_magma (X,n)), (
free_magma (X,m)):],
{n}:], y be
Element of (
free_magma (X,n)), z be
Element of (
free_magma (X,m)) st y
= ((x
`1 )
`1 ) & z
= ((x
`1 )
`2 ) holds (f2
. x)
= ((f
. y)
* (g
. z));
for x be
object st x
in
[:
[:(
free_magma (X,n)), (
free_magma (X,m)):],
{n}:] holds (f1
. x)
= (f2
. x)
proof
let x be
object;
assume x
in
[:
[:(
free_magma (X,n)), (
free_magma (X,m)):],
{n}:];
then
reconsider x9 = x as
Element of
[:
[:(
free_magma (X,n)), (
free_magma (X,m)):],
{n}:];
A6: (x9
`1 )
in
[:(
free_magma (X,n)), (
free_magma (X,m)):] by
MCART_1: 10;
then
reconsider x1 = ((x9
`1 )
`1 ) as
Element of (
free_magma (X,n)) by
MCART_1: 10;
reconsider x2 = ((x9
`1 )
`2 ) as
Element of (
free_magma (X,m)) by
A6,
MCART_1: 10;
thus (f1
. x)
= ((f
. x1)
* (g
. x2)) by
A4
.= (f2
. x) by
A5;
end;
hence thesis by
FUNCT_2: 12;
end;
end
reserve M for non
empty
multMagma;
theorem ::
ALGSTR_4:39
Th39: for f be
Function of X, M holds ex h be
Function of (
free_magma X), M st h is
multiplicative & h
extends (f
* ((
canon_image (X,1))
" ))
proof
let f be
Function of X, M;
defpred
P1[
object,
object] means ex n st n
= $1 & $2
= (
Funcs ((
free_magma (X,n)),the
carrier of M));
A1: for x be
object st x
in
NAT holds ex y be
object st
P1[x, y]
proof
let x be
object;
assume x
in
NAT ;
then
reconsider n = x as
Nat;
set y = (
Funcs ((
free_magma (X,n)),the
carrier of M));
take y;
thus
P1[x, y];
end;
consider F1 be
Function such that
A2: (
dom F1)
=
NAT & for x be
object st x
in
NAT holds
P1[x, (F1
. x)] from
CLASSES1:sch 1(
A1);
A3: f
in (
Funcs (X,the
carrier of M)) by
FUNCT_2: 8;
P1[1, (F1
. 1)] by
A2;
then (F1
. 1)
= (
Funcs (X,the
carrier of M)) by
Def13;
then (
Funcs (X,the
carrier of M))
in (
rng F1) by
A2,
FUNCT_1: 3;
then
A4: f
in (
union (
rng F1)) by
A3,
TARSKI:def 4;
then
A5: f
in (
Union F1) by
CARD_3:def 4;
reconsider X1 = (
Union F1) as non
empty
set by
A4,
CARD_3:def 4;
defpred
P2[
object,
object] means for fs be
XFinSequence of X1 st $1
= fs holds (((for m be non
zero
Nat st m
in (
dom fs) holds (fs
. m) is
Function of (
free_magma (X,m)), M) implies (((
dom fs)
=
0 implies $2
=
{} ) & ((
dom fs)
= 1 implies $2
= f) & for n be
Nat st n
>= 2 & (
dom fs)
= n holds ex fs1 be
FinSequence st (
len fs1)
= (n
- 1) & (for p be
Nat st p
>= 1 & p
<= (n
- 1) holds ex m1,m2 be non
zero
Nat, f1 be
Function of (
free_magma (X,m1)), M, f2 be
Function of (
free_magma (X,m2)), M st m1
= p & m2
= (n
- p) & f1
= (fs
. m1) & f2
= (fs
. m2) & (fs1
. p)
=
[:f1, f2:]) & $2
= (
Union fs1))) & ( not (for m be non
zero
Nat st m
in (
dom fs) holds (fs
. m) is
Function of (
free_magma (X,m)), M) implies $2
= f));
A6: for e be
object st e
in (X1
^omega ) holds ex u be
object st
P2[e, u]
proof
let e be
object;
assume e
in (X1
^omega );
then
reconsider fs = e as
XFinSequence of X1 by
AFINSQ_1:def 7;
per cases ;
suppose
A7: for m be non
zero
Nat st m
in (
dom fs) holds (fs
. m) is
Function of (
free_magma (X,m)), M;
(
dom fs)
=
0 or ((
dom fs)
+ 1)
> (
0
+ 1) by
XREAL_1: 6;
then (
dom fs)
=
0 or (
dom fs)
>= 1 by
NAT_1: 13;
then (
dom fs)
=
0 or (
dom fs)
= 1 or (
dom fs)
> 1 by
XXREAL_0: 1;
then
A8: (
dom fs)
=
0 or (
dom fs)
= 1 or ((
dom fs)
+ 1)
> (1
+ 1) by
XREAL_1: 6;
per cases by
A8,
NAT_1: 13;
suppose
A9: (
dom fs)
=
0 ;
set u =
{} ;
take u;
thus
P2[e, u] by
A9;
end;
suppose
A10: (
dom fs)
= 1;
set u = f;
take u;
thus
P2[e, u] by
A10;
end;
suppose
A11: (
dom fs)
>= 2;
reconsider n = (
dom fs) as
Nat;
reconsider n9 = (n
-' 1) as
Nat;
(n
- 1)
>= (2
- 1) by
A11,
XREAL_1: 9;
then
A12: n9
= (n
- 1) by
XREAL_0:def 2;
A13: (
Seg n9)
c= (
Segm (n9
+ 1)) by
AFINSQ_1: 3;
defpred
P3[
set,
object] means for p be
Nat st p
>= 1 & p
<= (n
- 1) & $1
= p holds ex m1,m2 be non
zero
Nat, f1 be
Function of (
free_magma (X,m1)), M, f2 be
Function of (
free_magma (X,m2)), M st m1
= p & m2
= (n
- p) & f1
= (fs
. m1) & f2
= (fs
. m2) & $2
=
[:f1, f2:];
A14: for k be
Nat st k
in (
Seg n9) holds ex x be
object st
P3[k, x]
proof
let k be
Nat;
assume
A15: k
in (
Seg n9);
then
A16: 1
<= k & k
<= n9 by
FINSEQ_1: 1;
then (k
+ 1)
<= ((n
- 1)
+ 1) by
A12,
XREAL_1: 7;
then
A17: ((k
+ 1)
- k)
<= (n
- k) by
XREAL_1: 9;
then
A18: (n
-' k)
= (n
- k) by
XREAL_0:def 2;
reconsider m1 = k as non
zero
Nat by
A15,
FINSEQ_1: 1;
reconsider m2 = (n
- k) as non
zero
Nat by
A17,
A18;
reconsider f1 = (fs
. m1) as
Function of (
free_magma (X,m1)), M by
A7,
A15,
A13,
A12;
(
- 1)
>= (
- k) by
A16,
XREAL_1: 24;
then ((
- 1)
+ n)
>= ((
- k)
+ n) by
XREAL_1: 7;
then m2
in (
Seg n9) by
A12,
A17,
FINSEQ_1: 1;
then
reconsider f2 = (fs
. m2) as
Function of (
free_magma (X,m2)), M by
A7,
A13,
A12;
set x =
[:f1, f2:];
take x;
thus thesis;
end;
consider fs1 be
FinSequence such that
A19: (
dom fs1)
= (
Seg n9) & for k be
Nat st k
in (
Seg n9) holds
P3[k, (fs1
. k)] from
FINSEQ_1:sch 1(
A14);
set u = (
Union fs1);
take u;
now
assume for m be non
zero
Nat st m
in (
dom fs) holds (fs
. m) is
Function of (
free_magma (X,m)), M;
thus ((
dom fs)
=
0 implies u
=
{} ) & ((
dom fs)
= 1 implies u
= f) by
A11;
thus for n be
Nat st n
>= 2 & (
dom fs)
= n holds ex fs1 be
FinSequence st (
len fs1)
= (n
- 1) & (for p be
Nat st p
>= 1 & p
<= (n
- 1) holds ex m1,m2 be non
zero
Nat, f1 be
Function of (
free_magma (X,m1)), M, f2 be
Function of (
free_magma (X,m2)), M st m1
= p & m2
= (n
- p) & f1
= (fs
. m1) & f2
= (fs
. m2) & (fs1
. p)
=
[:f1, f2:]) & u
= (
Union fs1)
proof
let n99 be
Nat;
assume n99
>= 2;
assume
A20: (
dom fs)
= n99;
take fs1;
thus (
len fs1)
= (n99
- 1) by
A12,
A20,
A19,
FINSEQ_1:def 3;
thus for p be
Nat st p
>= 1 & p
<= (n99
- 1) holds ex m1,m2 be non
zero
Nat, f1 be
Function of (
free_magma (X,m1)), M, f2 be
Function of (
free_magma (X,m2)), M st m1
= p & m2
= (n99
- p) & f1
= (fs
. m1) & f2
= (fs
. m2) & (fs1
. p)
=
[:f1, f2:] by
A20,
FINSEQ_1: 1,
A12,
A19;
thus u
= (
Union fs1);
end;
end;
hence thesis by
A7;
end;
end;
suppose
A21: not for m be non
zero
Nat st m
in (
dom fs) holds (fs
. m) is
Function of (
free_magma (X,m)), M;
take f;
thus thesis by
A21;
end;
end;
consider F2 be
Function such that
A22: (
dom F2)
= (X1
^omega ) & for e be
object st e
in (X1
^omega ) holds
P2[e, (F2
. e)] from
CLASSES1:sch 1(
A6);
A23: for n be
Nat, fs be
XFinSequence of X1 st n
>= 2 & (
dom fs)
= n & (for m be non
zero
Nat st m
in (
dom fs) holds (fs
. m) is
Function of (
free_magma (X,m)), M) & (ex fs1 be
FinSequence st (
len fs1)
= (n
- 1) & (for p be
Nat st p
>= 1 & p
<= (n
- 1) holds ex m1,m2 be non
zero
Nat, f1 be
Function of (
free_magma (X,m1)), M, f2 be
Function of (
free_magma (X,m2)), M st m1
= p & m2
= (n
- p) & f1
= (fs
. m1) & f2
= (fs
. m2) & (fs1
. p)
=
[:f1, f2:]) & (F2
. fs)
= (
Union fs1)) holds (F2
. fs)
in (
Funcs ((
free_magma (X,n)),the
carrier of M))
proof
let n be
Nat;
let fs be
XFinSequence of X1;
assume
A24: n
>= 2;
assume (
dom fs)
= n;
assume for m be non
zero
Nat st m
in (
dom fs) holds (fs
. m) is
Function of (
free_magma (X,m)), M;
assume ex fs1 be
FinSequence st (
len fs1)
= (n
- 1) & (for p be
Nat st p
>= 1 & p
<= (n
- 1) holds ex m1,m2 be non
zero
Nat, f1 be
Function of (
free_magma (X,m1)), M, f2 be
Function of (
free_magma (X,m2)), M st m1
= p & m2
= (n
- p) & f1
= (fs
. m1) & f2
= (fs
. m2) & (fs1
. p)
=
[:f1, f2:]) & (F2
. fs)
= (
Union fs1);
then
consider fs1 be
FinSequence such that
A25: (
len fs1)
= (n
- 1) and
A26: for p be
Nat st p
>= 1 & p
<= (n
- 1) holds ex m1,m2 be non
zero
Nat, f1 be
Function of (
free_magma (X,m1)), M, f2 be
Function of (
free_magma (X,m2)), M st m1
= p & m2
= (n
- p) & f1
= (fs
. m1) & f2
= (fs
. m2) & (fs1
. p)
=
[:f1, f2:] and
A27: (F2
. fs)
= (
Union fs1);
A28: for x be
object st x
in (F2
. fs) holds ex y,z be
object st x
=
[y, z]
proof
let x be
object;
assume x
in (F2
. fs);
then x
in (
union (
rng fs1)) by
A27,
CARD_3:def 4;
then
consider Y be
set such that
A29: x
in Y & Y
in (
rng fs1) by
TARSKI:def 4;
consider p be
object such that
A30: p
in (
dom fs1) & Y
= (fs1
. p) by
A29,
FUNCT_1:def 3;
reconsider p as
Nat by
A30;
p
in (
Seg (
len fs1)) by
A30,
FINSEQ_1:def 3;
then 1
<= p & p
<= (n
- 1) by
A25,
FINSEQ_1: 1;
then
consider m1,m2 be non
zero
Nat, f1 be
Function of (
free_magma (X,m1)), M, f2 be
Function of (
free_magma (X,m2)), M such that
A31: m1
= p & m2
= (n
- p) & f1
= (fs
. m1) & f2
= (fs
. m2) & (fs1
. p)
=
[:f1, f2:] by
A26;
consider y,z be
object such that
A32: x
=
[y, z] by
A29,
A30,
A31,
RELAT_1:def 1;
take y, z;
thus x
=
[y, z] by
A32;
end;
for x,y1,y2 be
object st
[x, y1]
in (F2
. fs) &
[x, y2]
in (F2
. fs) holds y1
= y2
proof
let x,y1,y2 be
object;
assume
[x, y1]
in (F2
. fs);
then
[x, y1]
in (
union (
rng fs1)) by
A27,
CARD_3:def 4;
then
consider Y1 be
set such that
A33:
[x, y1]
in Y1 & Y1
in (
rng fs1) by
TARSKI:def 4;
consider p1 be
object such that
A34: p1
in (
dom fs1) & Y1
= (fs1
. p1) by
A33,
FUNCT_1:def 3;
reconsider p1 as
Nat by
A34;
p1
in (
Seg (
len fs1)) by
A34,
FINSEQ_1:def 3;
then 1
<= p1 & p1
<= (n
- 1) by
A25,
FINSEQ_1: 1;
then
consider m19,m29 be non
zero
Nat, f19 be
Function of (
free_magma (X,m19)), M, f29 be
Function of (
free_magma (X,m29)), M such that
A35: m19
= p1 & m29
= (n
- p1) & f19
= (fs
. m19) & f29
= (fs
. m29) & (fs1
. p1)
=
[:f19, f29:] by
A26;
A36: x
in (
dom
[:f19, f29:]) by
A33,
A34,
A35,
FUNCT_1: 1;
then (x
`2 )
in
{m19} by
MCART_1: 10;
then
A37: (x
`2 )
= m19 by
TARSKI:def 1;
assume
[x, y2]
in (F2
. fs);
then
[x, y2]
in (
union (
rng fs1)) by
A27,
CARD_3:def 4;
then
consider Y2 be
set such that
A38:
[x, y2]
in Y2 & Y2
in (
rng fs1) by
TARSKI:def 4;
consider p2 be
object such that
A39: p2
in (
dom fs1) & Y2
= (fs1
. p2) by
A38,
FUNCT_1:def 3;
reconsider p2 as
Nat by
A39;
p2
in (
Seg (
len fs1)) by
A39,
FINSEQ_1:def 3;
then 1
<= p2 & p2
<= (n
- 1) by
A25,
FINSEQ_1: 1;
then
consider m199,m299 be non
zero
Nat, f199 be
Function of (
free_magma (X,m199)), M, f299 be
Function of (
free_magma (X,m299)), M such that
A40: m199
= p2 & m299
= (n
- p2) & f199
= (fs
. m199) & f299
= (fs
. m299) & (fs1
. p2)
=
[:f199, f299:] by
A26;
A41: x
in (
dom
[:f199, f299:]) by
A38,
A39,
A40,
FUNCT_1: 1;
then (x
`2 )
in
{m199} by
MCART_1: 10;
then
A42: f19
= f199 & f29
= f299 by
A35,
A40,
A37,
TARSKI:def 1;
A43: (x
`1 )
in
[:(
free_magma (X,m19)), (
free_magma (X,m29)):] by
A36,
MCART_1: 10;
reconsider x1 = x as
Element of
[:
[:(
free_magma (X,m19)), (
free_magma (X,m29)):],
{m19}:] by
A36;
reconsider y19 = ((x
`1 )
`1 ) as
Element of (
free_magma (X,m19)) by
A43,
MCART_1: 10;
reconsider z1 = ((x
`1 )
`2 ) as
Element of (
free_magma (X,m29)) by
A43,
MCART_1: 10;
A44: (x
`1 )
in
[:(
free_magma (X,m199)), (
free_magma (X,m299)):] by
A41,
MCART_1: 10;
reconsider x2 = x as
Element of
[:
[:(
free_magma (X,m199)), (
free_magma (X,m299)):],
{m199}:] by
A41;
reconsider y29 = ((x
`1 )
`1 ) as
Element of (
free_magma (X,m199)) by
A44,
MCART_1: 10;
reconsider z2 = ((x
`1 )
`2 ) as
Element of (
free_magma (X,m299)) by
A44,
MCART_1: 10;
thus y1
= (
[:f19, f29:]
. x1) by
A33,
A34,
A35,
FUNCT_1: 1
.= ((f19
. y19)
* (f29
. z1)) by
Def20
.= ((f199
. y29)
* (f299
. z2)) by
A42
.= (
[:f199, f299:]
. x2) by
Def20
.= y2 by
A38,
A39,
A40,
FUNCT_1: 1;
end;
then
reconsider f9 = (F2
. fs) as
Function by
A28,
FUNCT_1:def 1,
RELAT_1:def 1;
for x be
object holds x
in (
free_magma (X,n)) iff ex y be
object st
[x, y]
in f9
proof
let x be
object;
hereby
assume x
in (
free_magma (X,n));
then
consider p,m be
Nat such that
A45: (x
`2 )
= p & 1
<= p & p
<= (n
- 1) & ((x
`1 )
`1 )
in (
free_magma (X,p)) & ((x
`1 )
`2 )
in (
free_magma (X,m)) & n
= (p
+ m) & x
in
[:
[:(
free_magma (X,p)), (
free_magma (X,m)):],
{p}:] by
A24,
Th21;
consider m1,m2 be non
zero
Nat, f1 be
Function of (
free_magma (X,m1)), M, f2 be
Function of (
free_magma (X,m2)), M such that
A46: m1
= p & m2
= (n
- p) & f1
= (fs
. m1) & f2
= (fs
. m2) & (fs1
. p)
=
[:f1, f2:] by
A26,
A45;
reconsider x9 = x as
Element of
[:
[:(
free_magma (X,m1)), (
free_magma (X,m2)):],
{m1}:] by
A45,
A46;
reconsider y9 = ((x
`1 )
`1 ) as
Element of (
free_magma (X,m1)) by
A45,
A46;
reconsider z9 = ((x
`1 )
`2 ) as
Element of (
free_magma (X,m2)) by
A45,
A46;
reconsider y = ((f1
. y9)
* (f2
. z9)) as
object;
A47: (
dom
[:f1, f2:])
=
[:
[:(
free_magma (X,m1)), (
free_magma (X,m2)):],
{m1}:] by
FUNCT_2:def 1;
A48: (
[:f1, f2:]
. x9)
= y by
Def20;
take y;
A49:
[x, y]
in (fs1
. p) by
A46,
A47,
A48,
FUNCT_1: 1;
p
in (
Seg (
len fs1)) by
A45,
A25,
FINSEQ_1: 1;
then p
in (
dom fs1) by
FINSEQ_1:def 3;
then (fs1
. p)
in (
rng fs1) by
FUNCT_1: 3;
then
[x, y]
in (
union (
rng fs1)) by
A49,
TARSKI:def 4;
hence
[x, y]
in f9 by
A27,
CARD_3:def 4;
end;
given y be
object such that
A50:
[x, y]
in f9;
[x, y]
in (
union (
rng fs1)) by
A27,
A50,
CARD_3:def 4;
then
consider Y be
set such that
A51:
[x, y]
in Y & Y
in (
rng fs1) by
TARSKI:def 4;
consider p be
object such that
A52: p
in (
dom fs1) & Y
= (fs1
. p) by
A51,
FUNCT_1:def 3;
A53: p
in (
Seg (
len fs1)) by
A52,
FINSEQ_1:def 3;
reconsider p as
Nat by
A52;
p
>= 1 & p
<= (n
- 1) by
A53,
A25,
FINSEQ_1: 1;
then
consider m1,m2 be non
zero
Nat, f1 be
Function of (
free_magma (X,m1)), M, f2 be
Function of (
free_magma (X,m2)), M such that
A54: m1
= p & m2
= (n
- p) & f1
= (fs
. m1) & f2
= (fs
. m2) & (fs1
. p)
=
[:f1, f2:] by
A26;
A55: x
in (
dom
[:f1, f2:]) by
A51,
A52,
A54,
FUNCT_1: 1;
then
A56: (x
`1 )
in
[:(
free_magma (X,m1)), (
free_magma (X,m2)):] & (x
`2 )
in
{m1} by
MCART_1: 10;
then
A57: ((x
`1 )
`1 )
in (
free_magma (X,m1)) & ((x
`1 )
`2 )
in (
free_magma (X,m2)) by
MCART_1: 10;
x
=
[(x
`1 ), (x
`2 )] by
A55,
MCART_1: 21;
then
A58: x
=
[
[((x
`1 )
`1 ), ((x
`1 )
`2 )], (x
`2 )] by
A56,
MCART_1: 21;
(x
`2 )
= m1 by
A56,
TARSKI:def 1;
then x
in (
free_magma (X,(m1
+ m2))) by
A58,
Th22,
A57;
hence x
in (
free_magma (X,n)) by
A54;
end;
then
A59: (
dom f9)
= (
free_magma (X,n)) by
XTUPLE_0:def 12;
for y be
object st y
in (
rng f9) holds y
in the
carrier of M
proof
let y be
object;
assume y
in (
rng f9);
then
consider x be
object such that
A60: x
in (
dom f9) & y
= (f9
. x) by
FUNCT_1:def 3;
[x, y]
in (
Union fs1) by
A27,
A60,
FUNCT_1: 1;
then
[x, y]
in (
union (
rng fs1)) by
CARD_3:def 4;
then
consider Y be
set such that
A61:
[x, y]
in Y & Y
in (
rng fs1) by
TARSKI:def 4;
consider p be
object such that
A62: p
in (
dom fs1) & Y
= (fs1
. p) by
A61,
FUNCT_1:def 3;
A63: p
in (
Seg (
len fs1)) by
A62,
FINSEQ_1:def 3;
reconsider p as
Nat by
A62;
p
>= 1 & p
<= (n
- 1) by
A63,
A25,
FINSEQ_1: 1;
then
consider m1,m2 be non
zero
Nat, f1 be
Function of (
free_magma (X,m1)), M, f2 be
Function of (
free_magma (X,m2)), M such that
A64: m1
= p & m2
= (n
- p) & f1
= (fs
. m1) & f2
= (fs
. m2) & (fs1
. p)
=
[:f1, f2:] by
A26;
y
in (
rng
[:f1, f2:]) by
A61,
A62,
A64,
XTUPLE_0:def 13;
hence y
in the
carrier of M;
end;
then (
rng f9)
c= the
carrier of M;
hence thesis by
A59,
FUNCT_2:def 2;
end;
for e be
object st e
in (X1
^omega ) holds (F2
. e)
in X1
proof
let e be
object;
assume
A65: e
in (X1
^omega );
then
reconsider fs = e as
XFinSequence of X1 by
AFINSQ_1:def 7;
per cases ;
suppose
A66: for m be non
zero
Nat st m
in (
dom fs) holds (fs
. m) is
Function of (
free_magma (X,m)), M;
then
A67: ((
dom fs)
=
0 implies (F2
. e)
=
{} ) & ((
dom fs)
= 1 implies (F2
. e)
= f) & for n be
Nat st n
>= 2 & (
dom fs)
= n holds ex fs1 be
FinSequence st (
len fs1)
= (n
- 1) & (for p be
Nat st p
>= 1 & p
<= (n
- 1) holds ex m1,m2 be non
zero
Nat, f1 be
Function of (
free_magma (X,m1)), M, f2 be
Function of (
free_magma (X,m2)), M st m1
= p & m2
= (n
- p) & f1
= (fs
. m1) & f2
= (fs
. m2) & (fs1
. p)
=
[:f1, f2:]) & (F2
. e)
= (
Union fs1) by
A65,
A22;
(
dom fs)
=
0 or ((
dom fs)
+ 1)
> (
0
+ 1) by
XREAL_1: 6;
then (
dom fs)
=
0 or (
dom fs)
>= 1 by
NAT_1: 13;
then (
dom fs)
=
0 or (
dom fs)
= 1 or (
dom fs)
> 1 by
XXREAL_0: 1;
then
A68: (
dom fs)
=
0 or (
dom fs)
= 1 or ((
dom fs)
+ 1)
> (1
+ 1) by
XREAL_1: 6;
per cases by
A68,
NAT_1: 13;
suppose
A69: (
dom fs)
=
0 ;
(
Funcs (
{} ,the
carrier of M))
=
{
{} } by
FUNCT_5: 57;
then
A70:
{}
in (
Funcs (
{} ,the
carrier of M)) by
TARSKI:def 1;
P1[
0 , (F1
.
0 )] by
A2;
then (F1
.
0 )
= (
Funcs (
{} ,the
carrier of M)) by
Def13;
then (
Funcs (
{} ,the
carrier of M))
in (
rng F1) by
A2,
FUNCT_1: 3;
then
{}
in (
union (
rng F1)) by
A70,
TARSKI:def 4;
hence (F2
. e)
in X1 by
A69,
A67,
CARD_3:def 4;
end;
suppose (
dom fs)
= 1;
hence (F2
. e)
in X1 by
A5,
A66,
A65,
A22;
end;
suppose
A71: (
dom fs)
>= 2;
set n = (
dom fs);
ex fs1 be
FinSequence st (
len fs1)
= (n
- 1) & (for p be
Nat st p
>= 1 & p
<= (n
- 1) holds ex m1,m2 be non
zero
Nat, f1 be
Function of (
free_magma (X,m1)), M, f2 be
Function of (
free_magma (X,m2)), M st m1
= p & m2
= (n
- p) & f1
= (fs
. m1) & f2
= (fs
. m2) & (fs1
. p)
=
[:f1, f2:]) & (F2
. e)
= (
Union fs1) by
A66,
A71,
A65,
A22;
then
A72: (F2
. e)
in (
Funcs ((
free_magma (X,n)),the
carrier of M)) by
A23,
A71,
A66;
A73: n
in (
dom F1) by
A2,
ORDINAL1:def 12;
then
P1[n, (F1
. n)] by
A2;
then (
Funcs ((
free_magma (X,n)),the
carrier of M))
in (
rng F1) by
A73,
FUNCT_1: 3;
then (F2
. e)
in (
union (
rng F1)) by
A72,
TARSKI:def 4;
hence (F2
. e)
in X1 by
CARD_3:def 4;
end;
end;
suppose not (for m be non
zero
Nat st m
in (
dom fs) holds (fs
. m) is
Function of (
free_magma (X,m)), M);
hence (F2
. e)
in X1 by
A5,
A65,
A22;
end;
end;
then
reconsider F2 as
Function of (X1
^omega ), X1 by
A22,
FUNCT_2: 3;
deffunc
FX(
XFinSequence of X1) = (F2
. $1);
consider F3 be
sequence of X1 such that
A74: for n be
Nat holds (F3
. n)
=
FX(|) from
FuncRecursiveExist2;
A75: for n be
Nat st n
>
0 holds (F3
. n) is
Function of (
free_magma (X,n)), M
proof
defpred
P4[
Nat] means for n be
Nat st $1
= n & n
>
0 holds (F3
. n) is
Function of (
free_magma (X,n)), M;
A76: for k be
Nat st for n be
Nat st n
< k holds
P4[n] holds
P4[k]
proof
let k be
Nat;
assume
A77: for n be
Nat st n
< k holds
P4[n];
thus
P4[k]
proof
let n be
Nat;
assume
A78: k
= n;
assume n
>
0 ;
A79: for m be non
zero
Nat st m
in (
dom (F3
| n)) holds ((F3
| n)
. m) is
Function of (
free_magma (X,m)), M
proof
let m be non
zero
Nat;
assume
A80: m
in (
dom (F3
| n));
then
A81: ((F3
| n)
. m)
= (F3
. m) by
FUNCT_1: 47;
m
in (
Segm k) by
A78,
A80;
then m
< k by
NAT_1: 44;
hence ((F3
| n)
. m) is
Function of (
free_magma (X,m)), M by
A81,
A77;
end;
A82: (F3
| n)
in (X1
^omega ) by
AFINSQ_1:def 7;
reconsider fs = (F3
| n) as
XFinSequence of X1;
A83: ((
dom fs)
=
0 implies (F2
. fs)
=
{} ) & ((
dom fs)
= 1 implies (F2
. fs)
= f) & for n be
Nat st n
>= 2 & (
dom fs)
= n holds ex fs1 be
FinSequence st (
len fs1)
= (n
- 1) & (for p be
Nat st p
>= 1 & p
<= (n
- 1) holds ex m1,m2 be non
zero
Nat, f1 be
Function of (
free_magma (X,m1)), M, f2 be
Function of (
free_magma (X,m2)), M st m1
= p & m2
= (n
- p) & f1
= (fs
. m1) & f2
= (fs
. m2) & (fs1
. p)
=
[:f1, f2:]) & (F2
. fs)
= (
Union fs1) by
A79,
A82,
A22;
A84: n
in
NAT by
ORDINAL1:def 12;
(
dom F3)
=
NAT by
FUNCT_2:def 1;
then
A85: n
c= (
dom F3) by
A84,
ORDINAL1:def 2;
A86: (
dom fs)
= ((
dom F3)
/\ n) by
RELAT_1: 61
.= n by
A85,
XBOOLE_1: 28;
(F2
. fs) is
Function of (
free_magma (X,n)), M
proof
n
=
0 or (n
+ 1)
> (
0
+ 1) by
XREAL_1: 6;
then n
=
0 or n
>= 1 by
NAT_1: 13;
then n
=
0 or n
= 1 or n
> 1 by
XXREAL_0: 1;
then
A87: n
=
0 or n
= 1 or (n
+ 1)
> (1
+ 1) by
XREAL_1: 6;
per cases by
A87,
NAT_1: 13;
suppose
A88: n
=
0 ;
(
Funcs (
{} ,the
carrier of M))
=
{
{} } by
FUNCT_5: 57;
then (F2
. fs)
in (
Funcs (
{} ,the
carrier of M)) by
A88,
A83,
TARSKI:def 1;
then (F2
. fs)
in (
Funcs ((
free_magma (X,n)),the
carrier of M)) by
A88,
Def13;
then ex f be
Function st (F2
. fs)
= f & (
dom f)
= (
free_magma (X,n)) & (
rng f)
c= the
carrier of M by
FUNCT_2:def 2;
hence thesis by
FUNCT_2: 2;
end;
suppose
A89: n
= 1;
(
free_magma (X,1))
= X by
Def13;
hence thesis by
A79,
A82,
A22,
A89,
A86;
end;
suppose
A90: n
>= 2;
then ex fs1 be
FinSequence st (
len fs1)
= (n
- 1) & (for p be
Nat st p
>= 1 & p
<= (n
- 1) holds ex m1,m2 be non
zero
Nat, f1 be
Function of (
free_magma (X,m1)), M, f2 be
Function of (
free_magma (X,m2)), M st m1
= p & m2
= (n
- p) & f1
= (fs
. m1) & f2
= (fs
. m2) & (fs1
. p)
=
[:f1, f2:]) & (F2
. fs)
= (
Union fs1) by
A79,
A82,
A22,
A86;
then (F2
. fs)
in (
Funcs ((
free_magma (X,n)),the
carrier of M)) by
A23,
A90,
A86,
A79;
then ex f be
Function st (F2
. fs)
= f & (
dom f)
= (
free_magma (X,n)) & (
rng f)
c= the
carrier of M by
FUNCT_2:def 2;
hence thesis by
FUNCT_2: 2;
end;
end;
hence (F3
. n) is
Function of (
free_magma (X,n)), M by
A74;
end;
end;
for k be
Nat holds
P4[k] from
NAT_1:sch 4(
A76);
hence thesis;
end;
reconsider X9 = the
carrier of (
free_magma X) as
set;
defpred
P5[
object,
object] means for w be
Element of (
free_magma X), f9 be
Function of (
free_magma (X,(w
`2 ))), M st w
= $1 & f9
= (F3
. (w
`2 )) holds $2
= (f9
. (w
`1 ));
A91: for x be
object st x
in X9 holds ex y be
object st y
in the
carrier of M &
P5[x, y]
proof
let x be
object;
assume x
in X9;
then
reconsider w = x as
Element of (
free_magma X);
reconsider f9 = (F3
. (w
`2 )) as
Function of (
free_magma (X,(w
`2 ))), M by
A75;
set y = (f9
. (w
`1 ));
take y;
w
in
[:(
free_magma (X,(w
`2 ))),
{(w
`2 )}:] by
Th25;
then (w
`1 )
in (
free_magma (X,(w
`2 ))) by
MCART_1: 10;
hence y
in the
carrier of M by
FUNCT_2: 5;
thus
P5[x, y];
end;
consider h be
Function of X9, the
carrier of M such that
A92: for x be
object st x
in X9 holds
P5[x, (h
. x)] from
FUNCT_2:sch 1(
A91);
reconsider h as
Function of (
free_magma X), M;
take h;
for a,b be
Element of (
free_magma X) holds (h
. (a
* b))
= ((h
. a)
* (h
. b))
proof
let a,b be
Element of (
free_magma X);
reconsider fab = (F3
. ((a
* b)
`2 )) as
Function of (
free_magma (X,((a
* b)
`2 ))), M by
A75;
(a
* b)
=
[
[
[(a
`1 ), (b
`1 )], (a
`2 )], ((
length a)
+ (
length b))] by
Th31;
then
A93: ((a
* b)
`1 )
=
[
[(a
`1 ), (b
`1 )], (a
`2 )] & ((a
* b)
`2 )
= ((
length a)
+ (
length b));
then
A94: fab
= (F2
. (F3
| ((
length a)
+ (
length b)))) by
A74;
A95: (F3
| ((
length a)
+ (
length b)))
in (X1
^omega ) by
AFINSQ_1:def 7;
A96: for m be non
zero
Nat st m
in (
dom (F3
| ((
length a)
+ (
length b)))) holds ((F3
| ((
length a)
+ (
length b)))
. m) is
Function of (
free_magma (X,m)), M
proof
let m be non
zero
Nat;
assume
A97: m
in (
dom (F3
| ((
length a)
+ (
length b))));
(F3
. m) is
Function of (
free_magma (X,m)), M by
A75;
hence thesis by
A97,
FUNCT_1: 47;
end;
set n = ((
length a)
+ (
length b));
(
length a)
>= 1 & (
length b)
>= 1 by
Th32;
then
A98: ((
length a)
+ (
length b))
>= (1
+ 1) by
XREAL_1: 7;
A99: n
in
NAT by
ORDINAL1:def 12;
(
dom F3)
=
NAT by
FUNCT_2:def 1;
then
A100: n
c= (
dom F3) by
A99,
ORDINAL1:def 2;
(
dom (F3
| n))
= ((
dom F3)
/\ n) by
RELAT_1: 61
.= n by
A100,
XBOOLE_1: 28;
then
consider fs1 be
FinSequence such that
A101: (
len fs1)
= (n
- 1) and
A102: for p be
Nat st p
>= 1 & p
<= (n
- 1) holds ex m1,m2 be non
zero
Nat, f1 be
Function of (
free_magma (X,m1)), M, f2 be
Function of (
free_magma (X,m2)), M st m1
= p & m2
= (n
- p) & f1
= ((F3
| n)
. m1) & f2
= ((F3
| n)
. m2) & (fs1
. p)
=
[:f1, f2:] and
A103: fab
= (
Union fs1) by
A96,
A98,
A95,
A22,
A94;
(a
* b)
in
[:(
free_magma (X,((a
* b)
`2 ))),
{((a
* b)
`2 )}:] by
Th25;
then ((a
* b)
`1 )
in (
free_magma (X,((a
* b)
`2 ))) by
MCART_1: 10;
then ((a
* b)
`1 )
in (
dom fab) by
FUNCT_2:def 1;
then
[((a
* b)
`1 ), (fab
. ((a
* b)
`1 ))]
in (
Union fs1) by
A103,
FUNCT_1: 1;
then
[((a
* b)
`1 ), (fab
. ((a
* b)
`1 ))]
in (
union (
rng fs1)) by
CARD_3:def 4;
then
consider Y be
set such that
A104:
[((a
* b)
`1 ), (fab
. ((a
* b)
`1 ))]
in Y & Y
in (
rng fs1) by
TARSKI:def 4;
consider p be
object such that
A105: p
in (
dom fs1) & Y
= (fs1
. p) by
A104,
FUNCT_1:def 3;
A106: p
in (
Seg (
len fs1)) by
A105,
FINSEQ_1:def 3;
reconsider p as
Nat by
A105;
p
>= 1 & p
<= (n
- 1) by
A106,
A101,
FINSEQ_1: 1;
then
consider m1,m2 be non
zero
Nat, f1 be
Function of (
free_magma (X,m1)), M, f2 be
Function of (
free_magma (X,m2)), M such that
A107: m1
= p & m2
= (n
- p) & f1
= ((F3
| n)
. m1) & f2
= ((F3
| n)
. m2) & (fs1
. p)
=
[:f1, f2:] by
A102;
A108: ((a
* b)
`1 )
in (
dom
[:f1, f2:]) by
A107,
A104,
A105,
FUNCT_1: 1;
then (((a
* b)
`1 )
`1 )
in
[:(
free_magma (X,m1)), (
free_magma (X,m2)):] & (((a
* b)
`1 )
`2 )
in
{m1} by
MCART_1: 10;
then
A109:
[(a
`1 ), (b
`1 )]
in
[:(
free_magma (X,m1)), (
free_magma (X,m2)):] & (a
`2 )
in
{m1} by
A93;
then m1
= (a
`2 ) by
TARSKI:def 1;
then
A110: m1
= (
length a) by
Def18;
(
length b)
>= (
0
+ 1) by
Th32;
then ((
length b)
+ (
length a))
> (
0
+ (
length a)) by
XREAL_1: 6;
then
A111: m1
in (
Segm n) by
A110,
NAT_1: 44;
(
length a)
>= (
0
+ 1) by
Th32;
then ((
length a)
+ (
length b))
> (
0
+ (
length b)) by
XREAL_1: 6;
then
A112: m2
in (
Segm n) by
A110,
A107,
NAT_1: 44;
reconsider x = ((a
* b)
`1 ) as
Element of
[:
[:(
free_magma (X,m1)), (
free_magma (X,m2)):],
{m1}:] by
A108;
A113: (x
`1 )
in
[:(
free_magma (X,m1)), (
free_magma (X,m2)):] by
MCART_1: 10;
then
reconsider y = ((x
`1 )
`1 ) as
Element of (
free_magma (X,m1)) by
MCART_1: 10;
reconsider z = ((x
`1 )
`2 ) as
Element of (
free_magma (X,m2)) by
A113,
MCART_1: 10;
A114: (x
`1 )
=
[(a
`1 ), (b
`1 )] by
A93;
A115: (
[:f1, f2:]
. x)
= ((f1
. y)
* (f2
. z)) by
Def20;
A116: (h
. (a
* b))
= (fab
. ((a
* b)
`1 )) by
A92;
A117: (fab
. ((a
* b)
`1 ))
= (
[:f1, f2:]
. x) by
A107,
A104,
A105,
FUNCT_1: 1;
reconsider fa = (F3
. (a
`2 )) as
Function of (
free_magma (X,(a
`2 ))), M by
A75;
reconsider fb = (F3
. (b
`2 )) as
Function of (
free_magma (X,(b
`2 ))), M by
A75;
f1
= (F3
. m1) by
A107,
A111,
FUNCT_1: 49
.= fa by
A109,
TARSKI:def 1;
then
A118: (fa
. (a
`1 ))
= (f1
. y) by
A114;
f2
= (F3
. m2) by
A107,
A112,
FUNCT_1: 49
.= fb by
Def18,
A110,
A107;
then
A119: (fb
. (b
`1 ))
= (f2
. z) by
A114;
(h
. b)
= (fb
. (b
`1 )) by
A92;
hence (h
. (a
* b))
= ((h
. a)
* (h
. b)) by
A115,
A116,
A118,
A119,
A92,
A117;
end;
hence h is
multiplicative by
GROUP_6:def 6;
set fX = (
canon_image (X,1));
for x be
object st x
in (
dom (f
* (fX
" ))) holds x
in (
dom h)
proof
let x be
object;
assume
A120: x
in (
dom (f
* (fX
" )));
(
dom (f
* (fX
" )))
c= (
dom (fX
" )) by
RELAT_1: 25;
then x
in (
dom (fX
" )) by
A120;
then x
in (
rng fX) by
FUNCT_1: 33;
then x
in the
carrier of (
free_magma X);
hence x
in (
dom h) by
FUNCT_2:def 1;
end;
then
A121: (
dom (f
* (fX
" )))
c= (
dom h);
for x be
object st x
in ((
dom h)
/\ (
dom (f
* (fX
" )))) holds (h
. x)
= ((f
* (fX
" ))
. x)
proof
let x be
object;
assume x
in ((
dom h)
/\ (
dom (f
* (fX
" ))));
then
A122: x
in (
dom (f
* (fX
" ))) by
A121,
XBOOLE_1: 28;
A123: (
dom (f
* (fX
" )))
c= (
dom (fX
" )) by
RELAT_1: 25;
then x
in (
dom (fX
" )) by
A122;
then x
in (
rng fX) by
FUNCT_1: 33;
then
consider x9 be
object such that
A124: x9
in (
dom fX) & x
= (fX
. x9) by
FUNCT_1:def 3;
A125: 1
in
{1} by
TARSKI:def 1;
[:(
free_magma (X,1)),
{1}:]
c= (
free_magma_carrier X) by
Lm1;
then
A126:
[:X,
{1}:]
c= (
free_magma_carrier X) by
Def13;
A127: x9
in X by
A124,
Lm3;
A128: x
=
[x9, 1] by
A124,
Def19;
then x
in
[:X,
{1}:] by
A125,
A127,
ZFMISC_1:def 2;
then
reconsider w = x as
Element of (
free_magma X) by
A126;
A129: ((fX
" )
. x)
= x9 by
A124,
FUNCT_1: 34;
set f9 = (F3
. (w
`2 ));
reconsider f9 as
Function of (
free_magma (X,(w
`2 ))), M by
A75;
A130: f9
= (F3
. 1) by
A128
.=
FX(|) by
A74;
A131: for m be non
zero
Nat st m
in (
dom (F3
| 1)) holds ((F3
| 1)
. m) is
Function of (
free_magma (X,m)), M
proof
let m be non
zero
Nat;
assume m
in (
dom (F3
| 1));
then ((F3
| 1)
. m)
= (F3
. m) by
FUNCT_1: 47;
hence ((F3
| 1)
. m) is
Function of (
free_magma (X,m)), M by
A75;
end;
A132: (F3
| 1)
in (X1
^omega ) by
AFINSQ_1:def 7;
reconsider fs = (F3
| 1) as
XFinSequence of X1;
(
dom F3)
=
NAT by
FUNCT_2:def 1;
then
A133: 1
c= (
dom F3) by
ORDINAL1:def 2;
A134: (
dom fs)
= ((
dom F3)
/\ 1) by
RELAT_1: 61
.= 1 by
A133,
XBOOLE_1: 28;
thus (h
. x)
= (f9
. (w
`1 )) by
A92
.= (f9
. x9) by
A128
.= (f
. ((fX
" )
. x)) by
A129,
A130,
A134,
A131,
A132,
A22
.= ((f
* (fX
" ))
. x) by
A123,
A122,
FUNCT_1: 13;
end;
then h
tolerates (f
* (fX
" )) by
PARTFUN1:def 4;
hence h
extends (f
* ((
canon_image (X,1))
" )) by
A121;
end;
theorem ::
ALGSTR_4:40
Th40: for f be
Function of X, M, h,g be
Function of (
free_magma X), M st h is
multiplicative & h
extends (f
* ((
canon_image (X,1))
" )) & g is
multiplicative & g
extends (f
* ((
canon_image (X,1))
" )) holds h
= g
proof
let f be
Function of X, M;
let h,g be
Function of (
free_magma X), M;
assume
A1: h is
multiplicative;
assume
A2: h
extends (f
* ((
canon_image (X,1))
" ));
assume
A3: g is
multiplicative;
assume
A4: g
extends (f
* ((
canon_image (X,1))
" ));
defpred
P[
Nat] means for w be
Element of (
free_magma X) st (
length w)
= $1 holds (h
. w)
= (g
. w);
A5: for k be
Nat st for n be
Nat st n
< k holds
P[n] holds
P[k]
proof
let k be
Nat;
assume
A6: for n be
Nat st n
< k holds
P[n];
thus for w be
Element of (
free_magma X) st (
length w)
= k holds (h
. w)
= (g
. w)
proof
let w be
Element of (
free_magma X);
assume
A7: (
length w)
= k;
A8: w
=
[(w
`1 ), (w
`2 )] & (
length w)
>= 1 by
Th32;
then (
length w)
= 1 or (
length w)
> 1 by
XXREAL_0: 1;
then
A9: (
length w)
= 1 or ((
length w)
+ 1)
> (1
+ 1) by
XREAL_1: 8;
per cases by
A9,
NAT_1: 13;
suppose
A10: (
length w)
= 1;
set x = (w
`1 );
x
in { (w9
`1 ) where w9 be
Element of (
free_magma X) : (
length w9)
= 1 } by
A10;
then
A11: x
in X by
Th30;
A12: (
dom (f
* ((
canon_image (X,1))
" )))
c= (
dom h) & h
tolerates (f
* ((
canon_image (X,1))
" )) by
A2;
A13: (
dom (f
* ((
canon_image (X,1))
" )))
c= (
dom g) & g
tolerates (f
* ((
canon_image (X,1))
" )) by
A4;
A14: ((
canon_image (X,1))
. x)
=
[x, 1] by
A11,
Lm3
.= w by
Def18,
A8,
A10;
x
in (
dom (
canon_image (X,1))) by
A11,
Lm3;
then w
in (
rng (
canon_image (X,1))) by
A14,
FUNCT_1: 3;
then
A15: w
in (
dom ((
canon_image (X,1))
" )) by
FUNCT_1: 33;
X
c= (
dom f) by
FUNCT_2:def 1;
then (
dom (
canon_image (X,1)))
c= (
dom f) by
Lm3;
then (
rng ((
canon_image (X,1))
" ))
c= (
dom f) by
FUNCT_1: 33;
then w
in (
dom (f
* ((
canon_image (X,1))
" ))) by
A15,
RELAT_1: 27;
then w
in ((
dom h)
/\ (
dom (f
* ((
canon_image (X,1))
" )))) & w
in ((
dom g)
/\ (
dom (f
* ((
canon_image (X,1))
" )))) by
A12,
A13,
XBOOLE_1: 28;
then (h
. w)
= ((f
* ((
canon_image (X,1))
" ))
. w) & (g
. w)
= ((f
* ((
canon_image (X,1))
" ))
. w) by
A12,
A13,
PARTFUN1:def 4;
hence thesis;
end;
suppose (
length w)
>= 2;
then
consider w1,w2 be
Element of (
free_magma X) such that
A16: w
= (w1
* w2) & (
length w1)
< (
length w) & (
length w2)
< (
length w) by
Th34;
(h
. w1)
= (g
. w1) & (h
. w2)
= (g
. w2) by
A6,
A7,
A16;
then (h
. (w1
* w2))
= ((g
. w1)
* (g
. w2)) by
A1,
GROUP_6:def 6;
hence (h
. w)
= (g
. w) by
A16,
A3,
GROUP_6:def 6;
end;
end;
end;
A17: for k be
Nat holds
P[k] from
NAT_1:sch 4(
A5);
for w be
Element of (
free_magma X) holds (h
. w)
= (g
. w)
proof
let w be
Element of (
free_magma X);
reconsider k = (
length w) as
Nat;
P[k] by
A17;
hence (h
. w)
= (g
. w);
end;
then for x be
object st x
in the
carrier of (
free_magma X) holds (h
. x)
= (g
. x);
hence h
= g by
FUNCT_2: 12;
end;
reserve M,N for non
empty
multMagma,
f for
Function of M, N,
H for non
empty
multSubmagma of N,
R for
compatible
Equivalence_Relation of M;
theorem ::
ALGSTR_4:41
Th41: f is
multiplicative & the
carrier of H
= (
rng f) & R
= (
equ_kernel f) implies ex g be
Function of (M
./. R), H st f
= (g
* (
nat_hom R)) & g is
bijective & g is
multiplicative
proof
assume
A1: f is
multiplicative;
assume
A2: the
carrier of H
= (
rng f);
assume
A3: R
= (
equ_kernel f);
set g = (((
nat_hom R)
~ )
* f);
for x,y1,y2 be
object st
[x, y1]
in g &
[x, y2]
in g holds y1
= y2
proof
let x,y1,y2 be
object;
assume
[x, y1]
in g;
then
consider z1 be
object such that
A4:
[x, z1]
in ((
nat_hom R)
~ ) &
[z1, y1]
in f by
RELAT_1:def 8;
assume
[x, y2]
in g;
then
consider z2 be
object such that
A5:
[x, z2]
in ((
nat_hom R)
~ ) &
[z2, y2]
in f by
RELAT_1:def 8;
A6:
[z1, x]
in (
nat_hom R) &
[z2, x]
in (
nat_hom R) by
A4,
A5,
RELAT_1:def 7;
then z1
in (
dom (
nat_hom R)) & z2
in (
dom (
nat_hom R)) by
XTUPLE_0:def 12;
then
reconsider z1, z2 as
Element of M;
A7: x
= ((
nat_hom R)
. z1) & x
= ((
nat_hom R)
. z2) by
A6,
FUNCT_1: 1;
A8: (f
. z1)
= y1 & (f
. z2)
= y2 by
A4,
A5,
FUNCT_1: 1;
((
nat_hom R)
. z1)
= (
Class (R,z1)) & ((
nat_hom R)
. z2)
= (
Class (R,z2)) by
Def6;
then z2
in (
Class (R,z1)) by
A7,
EQREL_1: 23;
then
[z1, z2]
in (
equ_kernel f) by
A3,
EQREL_1: 18;
hence y1
= y2 by
A8,
Def8;
end;
then
reconsider g as
Function by
FUNCT_1:def 1;
(
rng (
nat_hom R))
= the
carrier of (M
./. R) by
FUNCT_2:def 3;
then
A9: (
dom ((
nat_hom R)
~ ))
= the
carrier of (M
./. R) by
RELAT_1: 20;
the
carrier of M
c= (
dom f) by
FUNCT_2:def 1;
then (
dom (
nat_hom R))
c= (
dom f);
then (
rng ((
nat_hom R)
~ ))
c= (
dom f) by
RELAT_1: 20;
then
A10: (
dom g)
= the
carrier of (M
./. R) by
A9,
RELAT_1: 27;
(
dom f)
c= the
carrier of M;
then (
dom f)
c= (
dom (
nat_hom R)) by
FUNCT_2:def 1;
then (
dom f)
c= (
rng ((
nat_hom R)
~ )) by
RELAT_1: 20;
then
A11: (
rng g)
= the
carrier of H by
A2,
RELAT_1: 28;
then
reconsider g as
Function of (M
./. R), H by
A10,
FUNCT_2: 1;
take g;
for x1,x2 be
object st x1
in (
dom g) & x2
in (
dom g) & (g
. x1)
= (g
. x2) holds x1
= x2
proof
let x1,x2 be
object;
assume
A12: x1
in (
dom g);
assume
A13: x2
in (
dom g);
assume
A14: (g
. x1)
= (g
. x2);
set y = (g
. x1);
[x1, y]
in g by
A12,
FUNCT_1: 1;
then
consider z1 be
object such that
A15:
[x1, z1]
in ((
nat_hom R)
~ ) &
[z1, y]
in f by
RELAT_1:def 8;
[x2, y]
in g by
A14,
A13,
FUNCT_1: 1;
then
consider z2 be
object such that
A16:
[x2, z2]
in ((
nat_hom R)
~ ) &
[z2, y]
in f by
RELAT_1:def 8;
A17:
[z1, x1]
in (
nat_hom R) &
[z2, x2]
in (
nat_hom R) by
A15,
A16,
RELAT_1:def 7;
then z1
in (
dom (
nat_hom R)) & z2
in (
dom (
nat_hom R)) by
XTUPLE_0:def 12;
then
reconsider z1, z2 as
Element of M;
z1
in (
dom f) & z2
in (
dom f) & (f
. z1)
= y & (f
. z2)
= y by
A15,
A16,
FUNCT_1: 1;
then
[z1, z2]
in (
equ_kernel f) by
Def8;
then
A18: z2
in (
Class (R,z1)) by
A3,
EQREL_1: 18;
A19: ((
nat_hom R)
. z1)
= (
Class (R,z1)) & ((
nat_hom R)
. z2)
= (
Class (R,z2)) by
Def6;
x1
= ((
nat_hom R)
. z1) & x2
= ((
nat_hom R)
. z2) by
A17,
FUNCT_1: 1;
hence x1
= x2 by
A19,
A18,
EQREL_1: 23;
end;
then
A20: g is
one-to-one by
FUNCT_1:def 4;
A21: for x be
object holds x
in (
dom f) iff x
in (
dom (
nat_hom R)) & ((
nat_hom R)
. x)
in (
dom g)
proof
let x be
object;
hereby
assume x
in (
dom f);
then x
in the
carrier of M;
hence x
in (
dom (
nat_hom R)) by
FUNCT_2:def 1;
then ((
nat_hom R)
. x)
in (
rng (
nat_hom R)) by
FUNCT_1: 3;
then ((
nat_hom R)
. x)
in the
carrier of (M
./. R);
hence ((
nat_hom R)
. x)
in (
dom g) by
FUNCT_2:def 1;
end;
assume x
in (
dom (
nat_hom R)) & ((
nat_hom R)
. x)
in (
dom g);
then x
in the
carrier of M;
hence x
in (
dom f) by
FUNCT_2:def 1;
end;
for x be
object st x
in (
dom f) holds (f
. x)
= (g
. ((
nat_hom R)
. x))
proof
let x be
object;
assume
A22: x
in (
dom f);
set y = ((
nat_hom R)
. x);
y
in (
dom g) by
A22,
A21;
then
[y, (g
. y)]
in g by
FUNCT_1: 1;
then
consider z be
object such that
A23:
[y, z]
in ((
nat_hom R)
~ ) &
[z, (g
. y)]
in f by
RELAT_1:def 8;
[z, y]
in (
nat_hom R) by
A23,
RELAT_1:def 7;
then
A24: z
in (
dom (
nat_hom R)) & y
= ((
nat_hom R)
. z) by
FUNCT_1: 1;
A25: z
in (
dom f) & (g
. y)
= (f
. z) by
A23,
FUNCT_1: 1;
then
reconsider z9 = z, x9 = x as
Element of M by
A22;
((
nat_hom R)
. z9)
= (
Class (R,z9)) & ((
nat_hom R)
. x9)
= (
Class (R,x9)) by
Def6;
then z9
in (
Class (R,x9)) by
A24,
EQREL_1: 23;
then
[x, z]
in R by
EQREL_1: 18;
hence (f
. x)
= (g
. ((
nat_hom R)
. x)) by
A25,
A3,
Def8;
end;
hence f
= (g
* (
nat_hom R)) by
A21,
FUNCT_1: 10;
g is
onto by
A11,
FUNCT_2:def 3;
hence g is
bijective by
A20;
for v,w be
Element of (M
./. R) holds (g
. (v
* w))
= ((g
. v)
* (g
. w))
proof
let v,w be
Element of (M
./. R);
(v
* w)
in the
carrier of (M
./. R);
then (v
* w)
in (
dom g) by
FUNCT_2:def 1;
then
[(v
* w), (g
. (v
* w))]
in g by
FUNCT_1: 1;
then
consider z be
object such that
A26:
[(v
* w), z]
in ((
nat_hom R)
~ ) &
[z, (g
. (v
* w))]
in f by
RELAT_1:def 8;
[z, (v
* w)]
in (
nat_hom R) by
A26,
RELAT_1:def 7;
then
A27: z
in (
dom (
nat_hom R)) & ((
nat_hom R)
. z)
= (v
* w) by
FUNCT_1: 1;
A28: (f
. z)
= (g
. (v
* w)) by
A26,
FUNCT_1: 1;
v
in the
carrier of (M
./. R);
then v
in (
dom g) by
FUNCT_2:def 1;
then
[v, (g
. v)]
in g by
FUNCT_1: 1;
then
consider z1 be
object such that
A29:
[v, z1]
in ((
nat_hom R)
~ ) &
[z1, (g
. v)]
in f by
RELAT_1:def 8;
[z1, v]
in (
nat_hom R) by
A29,
RELAT_1:def 7;
then
A30: z1
in (
dom (
nat_hom R)) & ((
nat_hom R)
. z1)
= v by
FUNCT_1: 1;
A31: (f
. z1)
= (g
. v) by
A29,
FUNCT_1: 1;
w
in the
carrier of (M
./. R);
then w
in (
dom g) by
FUNCT_2:def 1;
then
[w, (g
. w)]
in g by
FUNCT_1: 1;
then
consider z2 be
object such that
A32:
[w, z2]
in ((
nat_hom R)
~ ) &
[z2, (g
. w)]
in f by
RELAT_1:def 8;
[z2, w]
in (
nat_hom R) by
A32,
RELAT_1:def 7;
then
A33: z2
in (
dom (
nat_hom R)) & ((
nat_hom R)
. z2)
= w by
FUNCT_1: 1;
A34: (f
. z2)
= (g
. w) by
A32,
FUNCT_1: 1;
reconsider z1, z2, z as
Element of M by
A30,
A33,
A27;
A35: ((
nat_hom R)
. z)
= ((
nat_hom R)
. (z1
* z2)) by
A30,
A33,
A27,
GROUP_6:def 6;
((
nat_hom R)
. (z1
* z2))
= (
Class (R,(z1
* z2))) & ((
nat_hom R)
. z)
= (
Class (R,z)) by
Def6;
then (z1
* z2)
in (
Class (R,z)) by
A35,
EQREL_1: 23;
then
[z, (z1
* z2)]
in R by
EQREL_1: 18;
then
A36: (f
. z)
= (f
. (z1
* z2)) by
A3,
Def8
.= ((f
. z1)
* (f
. z2)) by
A1,
GROUP_6:def 6;
A37:
[(g
. v), (g
. w)]
in
[:the
carrier of H, the
carrier of H:] by
ZFMISC_1:def 2;
thus (g
. (v
* w))
= (the
multF of N
.
[(g
. v), (g
. w)]) by
A31,
A34,
A36,
A28,
BINOP_1:def 1
.= ((the
multF of N
|
[:the
carrier of H, the
carrier of H:])
.
[(g
. v), (g
. w)]) by
A37,
FUNCT_1: 49
.= ((the
multF of N
|
[:the
carrier of H, the
carrier of H:])
. ((g
. v),(g
. w))) by
BINOP_1:def 1
.= ((the
multF of N
|| the
carrier of H)
. ((g
. v),(g
. w))) by
REALSET1:def 2
.= ((g
. v)
* (g
. w)) by
Def9;
end;
hence g is
multiplicative by
GROUP_6:def 6;
end;
theorem ::
ALGSTR_4:42
for g1,g2 be
Function of (M
./. R), N st (g1
* (
nat_hom R))
= (g2
* (
nat_hom R)) holds g1
= g2
proof
let g1,g2 be
Function of (M
./. R), N;
assume
A1: (g1
* (
nat_hom R))
= (g2
* (
nat_hom R));
set Y = (
rng (
nat_hom R));
(
rng (
nat_hom R))
= the
carrier of (M
./. R) by
FUNCT_2:def 3;
then (
dom g1)
= Y & (
dom g2)
= Y by
FUNCT_2:def 1;
hence g1
= g2 by
A1,
FUNCT_1: 86;
end;
theorem ::
ALGSTR_4:43
for M be non
empty
multMagma holds ex X be non
empty
set, r be
Relators of (
free_magma X), g be
Function of ((
free_magma X)
./. (
equ_rel r)), M st g is
bijective & g is
multiplicative
proof
let M be non
empty
multMagma;
set X = the
carrier of M;
consider f be
Function of (
free_magma X), M such that
A1: f is
multiplicative & f
extends ((
id X)
* ((
canon_image (X,1))
" )) by
Th39;
consider r be
Relators of (
free_magma X) such that
A2: (
equ_kernel f)
= (
equ_rel r) by
A1,
Th5;
reconsider R = (
equ_kernel f) as
compatible
Equivalence_Relation of (
free_magma X) by
A1,
Th4;
the
multF of M
= (the
multF of M
|
[:the
carrier of M, the
carrier of M:]);
then the
multF of M
= (the
multF of M
|| the
carrier of M) by
REALSET1:def 2;
then
reconsider H = M as non
empty
multSubmagma of M by
Def9;
for y be
object st y
in the
carrier of M holds ex x be
object st x
in (
dom f) & y
= (f
. x)
proof
let y be
object;
assume
A3: y
in the
carrier of M;
reconsider x =
[y, 1] as
set;
take x;
[:(
free_magma (X,1)),
{1}:]
c= the
carrier of (
free_magma X) by
Lm1;
then
A4:
[:X,
{1}:]
c= the
carrier of (
free_magma X) by
Def13;
1
in
{1} by
TARSKI:def 1;
then x
in
[:X,
{1}:] by
A3,
ZFMISC_1:def 2;
then x
in the
carrier of (
free_magma X) by
A4;
hence x
in (
dom f) by
FUNCT_2:def 1;
A5: (
dom ((
id X)
* ((
canon_image (X,1))
" )))
c= (
dom f) & f
tolerates ((
id X)
* ((
canon_image (X,1))
" )) by
A1;
A6: ((
canon_image (X,1))
. y)
= x by
A3,
Lm3;
y
in (
dom (
canon_image (X,1))) by
A3,
Lm3;
then x
in (
rng (
canon_image (X,1))) by
A6,
FUNCT_1: 3;
then
A7: x
in (
dom ((
canon_image (X,1))
" )) by
FUNCT_1: 33;
(
dom (
canon_image (X,1)))
c= (
dom (
id X)) by
Lm3;
then (
rng ((
canon_image (X,1))
" ))
c= (
dom (
id X)) by
FUNCT_1: 33;
then
A8: x
in (
dom ((
id X)
* ((
canon_image (X,1))
" ))) by
A7,
RELAT_1: 27;
A9: y
in (
dom (
canon_image (X,1))) by
A3,
Lm3;
thus y
= ((
id X)
. y) by
A3,
FUNCT_1: 18
.= ((
id X)
. (((
canon_image (X,1))
" )
. x)) by
A9,
A6,
FUNCT_1: 34
.= (((
id X)
* ((
canon_image (X,1))
" ))
. x) by
A8,
FUNCT_1: 12
.= (f
. x) by
A8,
A5,
PARTFUN1: 53;
end;
then the
carrier of M
c= (
rng f) by
FUNCT_1: 9;
then the
carrier of H
= (
rng f) by
XBOOLE_0:def 10;
then
consider g be
Function of ((
free_magma X)
./. R), H such that
A10: f
= (g
* (
nat_hom R)) & g is
bijective & g is
multiplicative by
A1,
Th41;
reconsider g as
Function of ((
free_magma X)
./. (
equ_rel r)), M by
A2;
take X, r, g;
thus thesis by
A10,
A2;
end;
definition
let X,Y be non
empty
set;
let f be
Function of X, Y;
::
ALGSTR_4:def21
func
free_magmaF f ->
Function of (
free_magma X), (
free_magma Y) means
:
Def21: it is
multiplicative & it
extends (((
canon_image (Y,1))
* f)
* ((
canon_image (X,1))
" ));
existence
proof
reconsider f9 = ((
canon_image (Y,1))
* f) as
Function of X, (
free_magma Y) by
Th38;
ex h be
Function of (
free_magma X), (
free_magma Y) st h is
multiplicative & h
extends (f9
* ((
canon_image (X,1))
" )) by
Th39;
hence thesis;
end;
uniqueness
proof
let f1,f2 be
Function of (
free_magma X), (
free_magma Y);
assume
A1: f1 is
multiplicative & f1
extends (((
canon_image (Y,1))
* f)
* ((
canon_image (X,1))
" ));
assume
A2: f2 is
multiplicative & f2
extends (((
canon_image (Y,1))
* f)
* ((
canon_image (X,1))
" ));
reconsider f9 = ((
canon_image (Y,1))
* f) as
Function of X, (
free_magma Y) by
Th38;
f1
extends (f9
* ((
canon_image (X,1))
" )) & f2
extends (f9
* ((
canon_image (X,1))
" )) by
A1,
A2;
hence f1
= f2 by
A1,
A2,
Th40;
end;
end
registration
let X,Y be non
empty
set;
let f be
Function of X, Y;
cluster (
free_magmaF f) ->
multiplicative;
coherence by
Def21;
end
reserve f for
Function of X, Y;
reserve g for
Function of Y, Z;
theorem ::
ALGSTR_4:44
Th44: (
free_magmaF (g
* f))
= ((
free_magmaF g)
* (
free_magmaF f))
proof
set f2 = ((
free_magmaF g)
* (
free_magmaF f));
reconsider f9 = ((
canon_image (Z,1))
* (g
* f)) as
Function of X, (
free_magma Z) by
Th38;
for a,b be
Element of (
free_magma X) holds (f2
. (a
* b))
= ((f2
. a)
* (f2
. b))
proof
let a,b be
Element of (
free_magma X);
(a
* b)
in the
carrier of (
free_magma X);
then
A1: (a
* b)
in (
dom f2) by
FUNCT_2:def 1;
a
in the
carrier of (
free_magma X) & b
in the
carrier of (
free_magma X);
then
A2: a
in (
dom (
free_magmaF f)) & b
in (
dom (
free_magmaF f)) by
FUNCT_2:def 1;
thus (f2
. (a
* b))
= ((
free_magmaF g)
. ((
free_magmaF f)
. (a
* b))) by
A1,
FUNCT_1: 12
.= ((
free_magmaF g)
. (((
free_magmaF f)
. a)
* ((
free_magmaF f)
. b))) by
GROUP_6:def 6
.= (((
free_magmaF g)
. ((
free_magmaF f)
. a))
* ((
free_magmaF g)
. ((
free_magmaF f)
. b))) by
GROUP_6:def 6
.= ((f2
. a)
* ((
free_magmaF g)
. ((
free_magmaF f)
. b))) by
A2,
FUNCT_1: 13
.= ((f2
. a)
* (f2
. b)) by
A2,
FUNCT_1: 13;
end;
then
A3: f2 is
multiplicative by
GROUP_6:def 6;
A4: (
dom (f9
* ((
canon_image (X,1))
" )))
c= (
dom ((
canon_image (X,1))
" )) by
RELAT_1: 25;
(
rng (
canon_image (X,1)))
c= the
carrier of (
free_magma X);
then (
dom ((
canon_image (X,1))
" ))
c= the
carrier of (
free_magma X) by
FUNCT_1: 33;
then (
dom (f9
* ((
canon_image (X,1))
" )))
c= the
carrier of (
free_magma X) by
A4;
then
A5: (
dom (f9
* ((
canon_image (X,1))
" )))
c= (
dom f2) by
FUNCT_2:def 1;
for x be
object st x
in (
dom (f9
* ((
canon_image (X,1))
" ))) holds (f2
. x)
= ((f9
* ((
canon_image (X,1))
" ))
. x)
proof
let x be
object;
assume
A6: x
in (
dom (f9
* ((
canon_image (X,1))
" )));
(
free_magmaF f)
extends (((
canon_image (Y,1))
* f)
* ((
canon_image (X,1))
" )) by
Def21;
then
A7: (
dom (((
canon_image (Y,1))
* f)
* ((
canon_image (X,1))
" )))
c= (
dom (
free_magmaF f)) & (((
canon_image (Y,1))
* f)
* ((
canon_image (X,1))
" ))
tolerates (
free_magmaF f);
A8: x
in (
dom ((
canon_image (X,1))
" )) by
A6,
FUNCT_1: 11;
X
c= (
dom f) by
FUNCT_2:def 1;
then (
dom (
canon_image (X,1)))
c= (
dom f) by
Lm3;
then (
rng ((
canon_image (X,1))
" ))
c= (
dom f) by
FUNCT_1: 33;
then
A9: x
in (
dom (f
* ((
canon_image (X,1))
" ))) by
A8,
RELAT_1: 27;
(
rng (f
* ((
canon_image (X,1))
" )))
c= Y;
then (
rng (f
* ((
canon_image (X,1))
" )))
c= (
dom (
canon_image (Y,1))) by
Lm3;
then x
in (
dom ((
canon_image (Y,1))
* (f
* ((
canon_image (X,1))
" )))) by
A9,
RELAT_1: 27;
then
A10: x
in (
dom (((
canon_image (Y,1))
* f)
* ((
canon_image (X,1))
" ))) by
RELAT_1: 36;
set y = ((f
* ((
canon_image (X,1))
" ))
. x);
(
free_magmaF g)
extends (((
canon_image (Z,1))
* g)
* ((
canon_image (Y,1))
" )) by
Def21;
then
A11: (
dom (((
canon_image (Z,1))
* g)
* ((
canon_image (Y,1))
" )))
c= (
dom (
free_magmaF g)) & (((
canon_image (Z,1))
* g)
* ((
canon_image (Y,1))
" ))
tolerates (
free_magmaF g);
y
in (
rng (f
* ((
canon_image (X,1))
" ))) by
A9,
FUNCT_1: 3;
then
A12: y
in Y;
then
A13: y
in (
dom (
canon_image (Y,1))) by
Lm3;
then
A14: ((
canon_image (Y,1))
. y)
in (
rng (
canon_image (Y,1))) by
FUNCT_1: 3;
Y
c= (
dom g) by
FUNCT_2:def 1;
then
A15: (
dom (
canon_image (Y,1)))
c= (
dom g) by
Lm3;
(
rng g)
c= Z;
then (
rng g)
c= (
dom (
canon_image (Z,1))) by
Lm3;
then (
dom (
canon_image (Y,1)))
c= (
dom ((
canon_image (Z,1))
* g)) by
A15,
RELAT_1: 27;
then
A16: (
rng ((
canon_image (Y,1))
" ))
c= (
dom ((
canon_image (Z,1))
* g)) by
FUNCT_1: 33;
(
rng (
canon_image (Y,1)))
c= (
dom ((
canon_image (Y,1))
" )) by
FUNCT_1: 33;
then
A17: (
rng (
canon_image (Y,1)))
c= (
dom (((
canon_image (Z,1))
* g)
* ((
canon_image (Y,1))
" ))) by
A16,
RELAT_1: 27;
A18: (
rng (
canon_image (Y,1)))
c= (
dom ((
canon_image (Y,1))
" )) by
FUNCT_1: 33;
(
dom (
canon_image (Y,1)))
= Y by
Lm3;
then
A19: y
in (
dom (((
canon_image (Y,1))
" )
* (
canon_image (Y,1)))) by
A12,
A18,
RELAT_1: 27;
A20: (((
canon_image (Z,1))
* g)
* (f
* ((
canon_image (X,1))
" )))
= ((
canon_image (Z,1))
* (g
* (f
* ((
canon_image (X,1))
" )))) by
RELAT_1: 36
.= ((
canon_image (Z,1))
* ((g
* f)
* ((
canon_image (X,1))
" ))) by
RELAT_1: 36
.= (((
canon_image (Z,1))
* (g
* f))
* ((
canon_image (X,1))
" )) by
RELAT_1: 36;
thus (f2
. x)
= ((
free_magmaF g)
. ((
free_magmaF f)
. x)) by
A6,
A5,
FUNCT_1: 12
.= ((
free_magmaF g)
. ((((
canon_image (Y,1))
* f)
* ((
canon_image (X,1))
" ))
. x)) by
A10,
A7,
PARTFUN1: 53
.= ((
free_magmaF g)
. (((
canon_image (Y,1))
* (f
* ((
canon_image (X,1))
" )))
. x)) by
RELAT_1: 36
.= ((
free_magmaF g)
. ((
canon_image (Y,1))
. ((f
* ((
canon_image (X,1))
" ))
. x))) by
A9,
FUNCT_1: 13
.= ((((
canon_image (Z,1))
* g)
* ((
canon_image (Y,1))
" ))
. ((
canon_image (Y,1))
. y)) by
A17,
A14,
A11,
PARTFUN1: 53
.= (((((
canon_image (Z,1))
* g)
* ((
canon_image (Y,1))
" ))
* (
canon_image (Y,1)))
. y) by
A13,
FUNCT_1: 13
.= ((((
canon_image (Z,1))
* g)
* (((
canon_image (Y,1))
" )
* (
canon_image (Y,1))))
. y) by
RELAT_1: 36
.= (((
canon_image (Z,1))
* g)
. ((((
canon_image (Y,1))
" )
* (
canon_image (Y,1)))
. y)) by
A19,
FUNCT_1: 13
.= (((
canon_image (Z,1))
* g)
. ((f
* ((
canon_image (X,1))
" ))
. x)) by
A13,
FUNCT_1: 34
.= ((f9
* ((
canon_image (X,1))
" ))
. x) by
A20,
A9,
FUNCT_1: 13;
end;
then f2
tolerates (f9
* ((
canon_image (X,1))
" )) by
A5,
PARTFUN1: 53;
then f2
extends (f9
* ((
canon_image (X,1))
" )) by
A5;
hence (
free_magmaF (g
* f))
= ((
free_magmaF g)
* (
free_magmaF f)) by
Def21,
A3;
end;
theorem ::
ALGSTR_4:45
Th45: for g be
Function of X, Z st Y
c= Z & f
= g holds (
free_magmaF f)
= (
free_magmaF g)
proof
let g be
Function of X, Z;
assume
A1: Y
c= Z;
assume
A2: f
= g;
A3: the
carrier of (
free_magma Y)
c= the
carrier of (
free_magma Z) by
A1,
Th27;
then
reconsider f9 = (
free_magmaF f) as
Function of (
free_magma X), (
free_magma Z) by
FUNCT_2: 7;
for a,b be
Element of (
free_magma X) holds (f9
. (a
* b))
= ((f9
. a)
* (f9
. b))
proof
let a,b be
Element of (
free_magma X);
set v = ((
free_magmaF f)
. a);
set w = ((
free_magmaF f)
. b);
reconsider v9 = v, w9 = w as
Element of (
free_magma Z) by
A3;
A4: (
length v)
= (v
`2 ) by
Def18
.= (
length v9) by
Def18;
A5: (
length w)
= (w
`2 ) by
Def18
.= (
length w9) by
Def18;
thus (f9
. (a
* b))
= (((
free_magmaF f)
. a)
* ((
free_magmaF f)
. b)) by
GROUP_6:def 6
.=
[
[
[(v9
`1 ), (w9
`1 )], (v9
`2 )], ((
length v9)
+ (
length w9))] by
Th31,
A4,
A5
.= ((f9
. a)
* (f9
. b)) by
Th31;
end;
then
A6: f9 is
multiplicative by
GROUP_6:def 6;
(
rng g)
c= Z;
then (
rng g)
c= (
dom (
canon_image (Z,1))) by
Lm3;
then
A7: (
dom ((
canon_image (Z,1))
* g))
= (
dom g) by
RELAT_1: 27;
X
c= (
dom g) by
FUNCT_2:def 1;
then (
dom (
canon_image (X,1)))
c= (
dom ((
canon_image (Z,1))
* g)) by
Lm3,
A7;
then (
rng ((
canon_image (X,1))
" ))
c= (
dom ((
canon_image (Z,1))
* g)) by
FUNCT_1: 33;
then
A8: (
dom (((
canon_image (Z,1))
* g)
* ((
canon_image (X,1))
" )))
= (
dom ((
canon_image (X,1))
" )) by
RELAT_1: 27;
(
rng (
canon_image (X,1)))
c= the
carrier of (
free_magma X);
then (
dom (((
canon_image (Z,1))
* g)
* ((
canon_image (X,1))
" )))
c= the
carrier of (
free_magma X) by
A8,
FUNCT_1: 33;
then
A9: (
dom (((
canon_image (Z,1))
* g)
* ((
canon_image (X,1))
" )))
c= (
dom f9) by
FUNCT_2:def 1;
for x be
object st x
in (
dom (((
canon_image (Z,1))
* g)
* ((
canon_image (X,1))
" ))) holds (f9
. x)
= ((((
canon_image (Z,1))
* g)
* ((
canon_image (X,1))
" ))
. x)
proof
let x be
object;
assume
A10: x
in (
dom (((
canon_image (Z,1))
* g)
* ((
canon_image (X,1))
" )));
(
free_magmaF f)
extends (((
canon_image (Y,1))
* f)
* ((
canon_image (X,1))
" )) by
Def21;
then
A11: (
dom (((
canon_image (Y,1))
* f)
* ((
canon_image (X,1))
" )))
c= (
dom (
free_magmaF f)) & (((
canon_image (Y,1))
* f)
* ((
canon_image (X,1))
" ))
tolerates (
free_magmaF f);
(
rng f)
c= Y;
then
A12: (
rng f)
c= (
dom (
canon_image (Y,1))) by
Lm3;
(
rng f)
c= Z by
A1;
then
A13: (
rng f)
c= (
dom (
canon_image (Z,1))) by
Lm3;
A14: (
dom ((
canon_image (Y,1))
* f))
= (
dom f) by
A12,
RELAT_1: 27
.= (
dom ((
canon_image (Z,1))
* f)) by
A13,
RELAT_1: 27;
for x be
object st x
in (
dom ((
canon_image (Y,1))
* f)) holds (((
canon_image (Y,1))
* f)
. x)
= (((
canon_image (Z,1))
* f)
. x)
proof
let x be
object;
assume
A15: x
in (
dom ((
canon_image (Y,1))
* f));
then
A16: (f
. x)
in (
dom (
canon_image (Y,1))) by
FUNCT_1: 11;
then
A17: (f
. x)
in Y by
Lm3;
thus (((
canon_image (Y,1))
* f)
. x)
= ((
canon_image (Y,1))
. (f
. x)) by
A15,
FUNCT_1: 12
.=
[(f
. x), 1] by
A16,
Def19
.= ((
canon_image (Z,1))
. (f
. x)) by
A1,
A17,
Lm3
.= (((
canon_image (Z,1))
* f)
. x) by
A14,
A15,
FUNCT_1: 12;
end;
then ((
canon_image (Y,1))
* f)
= ((
canon_image (Z,1))
* g) by
A2,
A14,
FUNCT_1: 2;
hence (f9
. x)
= ((((
canon_image (Z,1))
* g)
* ((
canon_image (X,1))
" ))
. x) by
A10,
A11,
PARTFUN1: 53;
end;
then f9
tolerates (((
canon_image (Z,1))
* g)
* ((
canon_image (X,1))
" )) by
A9,
PARTFUN1: 53;
then f9
extends (((
canon_image (Z,1))
* g)
* ((
canon_image (X,1))
" )) by
A9;
hence (
free_magmaF f)
= (
free_magmaF g) by
A6,
Def21;
end;
theorem ::
ALGSTR_4:46
Th46: (
free_magmaF (
id X))
= (
id (
dom (
free_magmaF f)))
proof
(
dom (
free_magmaF (
id X)))
= the
carrier of (
free_magma X) by
FUNCT_2:def 1;
then
A1: (
dom (
free_magmaF (
id X)))
= (
dom (
free_magmaF f)) by
FUNCT_2:def 1;
for x be
object st x
in (
dom (
free_magmaF f)) holds ((
free_magmaF (
id X))
. x)
= x
proof
let x be
object;
assume
A2: x
in (
dom (
free_magmaF f));
defpred
P[
Nat] means for w be
Element of (
free_magma X) st (
length w)
= $1 holds ((
free_magmaF (
id X))
. w)
= w;
A3: for k be
Nat st for n be
Nat st n
< k holds
P[n] holds
P[k]
proof
let k be
Nat;
assume
A4: for n be
Nat st n
< k holds
P[n];
thus for w be
Element of (
free_magma X) st (
length w)
= k holds ((
free_magmaF (
id X))
. w)
= w
proof
let w be
Element of (
free_magma X);
assume
A5: (
length w)
= k;
A6: w
=
[(w
`1 ), (w
`2 )] & (
length w)
>= 1 by
Th32;
then (
length w)
= 1 or (
length w)
> 1 by
XXREAL_0: 1;
then
A7: (
length w)
= 1 or ((
length w)
+ 1)
> (1
+ 1) by
XREAL_1: 8;
per cases by
A7,
NAT_1: 13;
suppose
A8: (
length w)
= 1;
set y = (w
`1 );
y
in { (w9
`1 ) where w9 be
Element of (
free_magma X) : (
length w9)
= 1 } by
A8;
then
A9: y
in X by
Th30;
then
A10: y
in (
dom (
id X));
(
free_magmaF (
id X))
extends (((
canon_image (X,1))
* (
id X))
* ((
canon_image (X,1))
" )) by
Def21;
then
A11: (
dom (((
canon_image (X,1))
* (
id X))
* ((
canon_image (X,1))
" )))
c= (
dom (
free_magmaF (
id X))) & (((
canon_image (X,1))
* (
id X))
* ((
canon_image (X,1))
" ))
tolerates (
free_magmaF (
id X));
A12: ((
canon_image (X,1))
. y)
=
[y, 1] by
A9,
Lm3
.= w by
Def18,
A6,
A8;
A13: y
in (
dom (
canon_image (X,1))) by
A9,
Lm3;
then w
in (
rng (
canon_image (X,1))) by
A12,
FUNCT_1: 3;
then
A14: w
in (
dom ((
canon_image (X,1))
" )) by
FUNCT_1: 33;
(
rng (
id X))
= X
.= (
dom (
canon_image (X,1))) by
Lm3;
then (
dom ((
canon_image (X,1))
* (
id X)))
= (
dom (
id X)) by
RELAT_1: 27;
then X
= (
dom ((
canon_image (X,1))
* (
id X)));
then (
dom (
canon_image (X,1)))
c= (
dom ((
canon_image (X,1))
* (
id X))) by
Lm3;
then (
rng ((
canon_image (X,1))
" ))
c= (
dom ((
canon_image (X,1))
* (
id X))) by
FUNCT_1: 33;
then
A15: w
in (
dom (((
canon_image (X,1))
* (
id X))
* ((
canon_image (X,1))
" ))) by
A14,
RELAT_1: 27;
(((
canon_image (X,1))
" )
. w)
= y by
A13,
A12,
FUNCT_1: 34;
then ((((
canon_image (X,1))
* (
id X))
* ((
canon_image (X,1))
" ))
. w)
= (((
canon_image (X,1))
* (
id X))
. y) by
A15,
FUNCT_1: 12
.= ((
canon_image (X,1))
. ((
id X)
. y)) by
A10,
FUNCT_1: 13
.= w by
A12,
A9,
FUNCT_1: 18;
hence ((
free_magmaF (
id X))
. w)
= w by
A15,
A11,
PARTFUN1: 53;
end;
suppose (
length w)
>= 2;
then
consider w1,w2 be
Element of (
free_magma X) such that
A16: w
= (w1
* w2) & (
length w1)
< (
length w) & (
length w2)
< (
length w) by
Th34;
thus ((
free_magmaF (
id X))
. w)
= (((
free_magmaF (
id X))
. w1)
* ((
free_magmaF (
id X))
. w2)) by
A16,
GROUP_6:def 6
.= (w1
* ((
free_magmaF (
id X))
. w2)) by
A4,
A5,
A16
.= w by
A4,
A5,
A16;
end;
end;
end;
A17: for k be
Nat holds
P[k] from
NAT_1:sch 4(
A3);
for w be
Element of (
free_magma X) holds ((
free_magmaF (
id X))
. w)
= w
proof
let w be
Element of (
free_magma X);
reconsider k = (
length w) as
Nat;
P[k] by
A17;
hence ((
free_magmaF (
id X))
. w)
= w;
end;
hence ((
free_magmaF (
id X))
. x)
= x by
A2;
end;
hence (
free_magmaF (
id X))
= (
id (
dom (
free_magmaF f))) by
A1,
FUNCT_1: 17;
end;
theorem ::
ALGSTR_4:47
f is
one-to-one implies (
free_magmaF f) is
one-to-one
proof
assume
A1: f is
one-to-one;
then
A2: ((f
" )
* f)
= (
id (
dom f)) by
FUNCT_1: 39;
set Y9 = (
rng f);
(
dom f)
= X by
FUNCT_2:def 1;
then
reconsider f1 = f as
Function of X, Y9 by
FUNCT_2: 1;
reconsider f2 = (f1
" ) as
Function of Y9, X by
A1,
FUNCT_2: 25;
(f2
* f1)
= (
id X) by
A2,
FUNCT_2:def 1;
then ((
free_magmaF f2)
* (
free_magmaF f1))
= (
free_magmaF (
id X)) by
Th44;
then ((
free_magmaF f2)
* (
free_magmaF f))
= (
free_magmaF (
id X)) by
Th45;
then ((
free_magmaF f2)
* (
free_magmaF f))
= (
id (
dom (
free_magmaF f))) by
Th46;
hence (
free_magmaF f) is
one-to-one by
FUNCT_1: 31;
end;
theorem ::
ALGSTR_4:48
f is
onto implies (
free_magmaF f) is
onto
proof
assume
A1: f is
onto;
for y be
object st y
in the
carrier of (
free_magma Y) holds y
in (
rng (
free_magmaF f))
proof
let y be
object;
assume
A2: y
in the
carrier of (
free_magma Y);
defpred
P[
Nat] means for w be
Element of (
free_magma Y) st (
length w)
= $1 holds ex v be
Element of (
free_magma X) st w
= ((
free_magmaF f)
. v);
A3: for k be
Nat st for n be
Nat st n
< k holds
P[n] holds
P[k]
proof
let k be
Nat;
assume
A4: for n be
Nat st n
< k holds
P[n];
thus for w be
Element of (
free_magma Y) st (
length w)
= k holds ex v be
Element of (
free_magma X) st w
= ((
free_magmaF f)
. v)
proof
let w be
Element of (
free_magma Y);
assume
A5: (
length w)
= k;
A6: w
=
[(w
`1 ), (w
`2 )] & (
length w)
>= 1 by
Th32;
then (
length w)
= 1 or (
length w)
> 1 by
XXREAL_0: 1;
then
A7: (
length w)
= 1 or ((
length w)
+ 1)
> (1
+ 1) by
XREAL_1: 8;
per cases by
A7,
NAT_1: 13;
suppose
A8: (
length w)
= 1;
set y = (w
`1 );
y
in { (w9
`1 ) where w9 be
Element of (
free_magma Y) : (
length w9)
= 1 } by
A8;
then
A9: y
in Y by
Th30;
(
free_magmaF f)
extends (((
canon_image (Y,1))
* f)
* ((
canon_image (X,1))
" )) by
Def21;
then
A10: (
dom (((
canon_image (Y,1))
* f)
* ((
canon_image (X,1))
" )))
c= (
dom (
free_magmaF f)) & (((
canon_image (Y,1))
* f)
* ((
canon_image (X,1))
" ))
tolerates (
free_magmaF f);
A11: ((
canon_image (Y,1))
. y)
=
[y, 1] by
A9,
Lm3
.= w by
Def18,
A6,
A8;
A12: (
rng f)
= Y by
A1,
FUNCT_2:def 3;
then
consider x be
object such that
A13: x
in (
dom f) & y
= (f
. x) by
A9,
FUNCT_1:def 3;
A14: 1
in
{1} by
TARSKI:def 1;
A15: x
in X by
A13;
then x
in (
free_magma (X,1)) by
Def13;
then
A16:
[x, 1]
in
[:(
free_magma (X,1)),
{1}:] by
A14,
ZFMISC_1:def 2;
[:(
free_magma (X,1)),
{1}:]
c= (
free_magma_carrier X) by
Lm1;
then
reconsider v =
[x, 1] as
Element of (
free_magma X) by
A16;
take v;
A17: x
in (
dom (
canon_image (X,1))) by
Lm3,
A15;
A18: v
= ((
canon_image (X,1))
. x) by
Lm3,
A13;
then v
in (
rng (
canon_image (X,1))) by
A17,
FUNCT_1: 3;
then
A19: v
in (
dom ((
canon_image (X,1))
" )) by
FUNCT_1: 33;
(
rng f)
= (
dom (
canon_image (Y,1))) by
Lm3,
A12;
then (
dom f)
= (
dom ((
canon_image (Y,1))
* f)) by
RELAT_1: 27;
then X
c= (
dom ((
canon_image (Y,1))
* f)) by
FUNCT_2:def 1;
then (
dom (
canon_image (X,1)))
c= (
dom ((
canon_image (Y,1))
* f)) by
Lm3;
then (
rng ((
canon_image (X,1))
" ))
c= (
dom ((
canon_image (Y,1))
* f)) by
FUNCT_1: 33;
then
A20: v
in (
dom (((
canon_image (Y,1))
* f)
* ((
canon_image (X,1))
" ))) by
A19,
RELAT_1: 27;
then
A21: ((
free_magmaF f)
. v)
= ((((
canon_image (Y,1))
* f)
* ((
canon_image (X,1))
" ))
. v) by
A10,
PARTFUN1: 53
.= (((
canon_image (Y,1))
* f)
. (((
canon_image (X,1))
" )
. v)) by
A20,
FUNCT_1: 12;
x
in (
dom (
canon_image (X,1))) by
A15,
Lm3;
then (((
canon_image (X,1))
" )
. v)
= x by
A18,
FUNCT_1: 34;
hence thesis by
A11,
A13,
A21,
FUNCT_1: 13;
end;
suppose (
length w)
>= 2;
then
consider w1,w2 be
Element of (
free_magma Y) such that
A22: w
= (w1
* w2) & (
length w1)
< (
length w) & (
length w2)
< (
length w) by
Th34;
consider v1 be
Element of (
free_magma X) such that
A23: w1
= ((
free_magmaF f)
. v1) by
A22,
A4,
A5;
consider v2 be
Element of (
free_magma X) such that
A24: w2
= ((
free_magmaF f)
. v2) by
A22,
A4,
A5;
take (v1
* v2);
thus thesis by
A23,
A24,
A22,
GROUP_6:def 6;
end;
end;
end;
A25: for k be
Nat holds
P[k] from
NAT_1:sch 4(
A3);
A26: for w be
Element of (
free_magma Y) holds ex v be
Element of (
free_magma X) st w
= ((
free_magmaF f)
. v)
proof
let w be
Element of (
free_magma Y);
reconsider k = (
length w) as
Nat;
P[k] by
A25;
hence thesis;
end;
ex x st x
in (
dom (
free_magmaF f)) & y
= ((
free_magmaF f)
. x)
proof
consider x be
Element of (
free_magma X) such that
A27: y
= ((
free_magmaF f)
. x) by
A2,
A26;
take x;
x
in the
carrier of (
free_magma X);
hence x
in (
dom (
free_magmaF f)) by
FUNCT_2:def 1;
thus y
= ((
free_magmaF f)
. x) by
A27;
end;
hence y
in (
rng (
free_magmaF f)) by
FUNCT_1:def 3;
end;
then the
carrier of (
free_magma Y)
c= (
rng (
free_magmaF f));
then (
rng (
free_magmaF f))
= the
carrier of (
free_magma Y) by
XBOOLE_0:def 10;
hence (
free_magmaF f) is
onto by
FUNCT_2:def 3;
end;