let X be non empty set ; :: thesis: for M being non empty multMagma
for f being Function of X,M ex h being Function of (free_magma X),M st
( h is multiplicative & h extends f * ((canon_image (X,1)) ") )
let M be non empty multMagma ; :: thesis: for f being Function of X,M ex h being Function of (free_magma X),M st
( h is multiplicative & h extends f * ((canon_image (X,1)) ") )
let f be Function of X,M; :: thesis: ex h being Function of (free_magma X),M st
( h is multiplicative & h extends f * ((canon_image (X,1)) ") )
defpred S1[ set , set ] means ex n being natural number st
( n = $1 & $2 = Funcs ((free_magma (X,n)), the carrier of M) );
A1: for x being set st x in NAT holds
ex y being set st S1[x,y]
proof
let x be set ; :: thesis: ( x in NAT implies ex y being set st S1[x,y] )
assume x in NAT ; :: thesis: ex y being set st S1[x,y]
then reconsider n = x as natural number ;
set y = Funcs ((free_magma (X,n)), the carrier of M);
take Funcs ((free_magma (X,n)), the carrier of M) ; :: thesis: S1[x, Funcs ((free_magma (X,n)), the carrier of M)]
thus S1[x, Funcs ((free_magma (X,n)), the carrier of M)] ; :: thesis: verum
end;
consider F1 being Function such that
A2: ( dom F1 = NAT & ( for x being set st x in NAT holds
S1[x,F1 . x] ) ) from CLASSES1:sch 1(A1);
 A3: f in Funcs (X, the carrier of M) by FUNCT_2:8;
S1[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 S2[ set , set ] means for fs being XFinSequence of st $1 = fs holds
( ( ( for m being non zero natural number 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 being natural number st n >= 2 & dom fs = n holds
ex fs1 being FinSequence st
( len fs1 = n - 1 & ( for p being natural number st p >= 1 & p <= n - 1 holds
ex m1, m2 being non zero natural number ex f1 being Function of (free_magma (X,m1)),M ex f2 being 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 ) ) ) ) & ( ex m being non zero natural number st
( m in dom fs & fs . m is not Function of (free_magma (X,m)),M ) implies $2 = f ) );
A6: for e being set st e in X1 ^omega holds
ex u being set st S2[e,u]
proof
let e be set ; :: thesis: ( e in X1 ^omega implies ex u being set st S2[e,u] )
assume e in X1 ^omega ; :: thesis: ex u being set st S2[e,u]
then reconsider fs = e as XFinSequence of by AFINSQ_1:def 7;
per cases ( for m being non zero natural number st m in dom fs holds
fs . m is Function of (free_magma (X,m)),M or ex m being non zero natural number st
( m in dom fs & fs . m is not Function of (free_magma (X,m)),M ) ) ;
suppose A7: for m being non zero natural number st m in dom fs holds
fs . m is Function of (free_magma (X,m)),M ; :: thesis: ex u being set st S2[e,u]
( 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 ( dom fs = 0 or dom fs = 1 or dom fs >= 2 ) by A8, NAT_1:13;
suppose A9: dom fs = 0 ; :: thesis: ex u being set st S2[e,u]
set u = {} ;
take {} ; :: thesis: S2[e, {} ]
thus S2[e, {} ] by A9; :: thesis: verum
end;
suppose A10: dom fs = 1 ; :: thesis: ex u being set st S2[e,u]
set u = f;
take f ; :: thesis: S2[e,f]
thus S2[e,f] by A10; :: thesis: verum
end;
suppose A11: dom fs >= 2 ; :: thesis: ex u being set st S2[e,u]
reconsider n = dom fs as natural number ;
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= n9 + 1 by AFINSQ_1:3;
defpred S3[ set , set ] means for p being natural number st p >= 1 & p <= n - 1 & $1 = p holds
ex m1, m2 being non zero natural number ex f1 being Function of (free_magma (X,m1)),M ex f2 being 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 being Nat st k in Seg n9 holds
ex x being set st S3[k,x]
proof
let k be Nat; :: thesis: ( k in Seg n9 implies ex x being set st S3[k,x] )
assume A15: k in Seg n9 ; :: thesis: ex x being set st S3[k,x]
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 natural number by A15, FINSEQ_1:1;
reconsider m2 = n - k as non zero natural number 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 [:f1,f2:] ; :: thesis: S3[k,[:f1,f2:]]
thus S3[k,[:f1,f2:]] ; :: thesis: verum
end;
consider fs1 being FinSequence such that
A19: ( dom fs1 = Seg n9 & ( for k being Nat st k in Seg n9 holds
S3[k,fs1 . k] ) ) from FINSEQ_1:sch 1(A14);
set u = Union fs1;
take Union fs1 ; :: thesis: S2[e, Union fs1]
now
assume for m being non zero natural number st m in dom fs holds
fs . m is Function of (free_magma (X,m)),M ; :: thesis: ( ( dom fs = 0 implies Union fs1 = {} ) & ( dom fs = 1 implies Union fs1 = f ) & ( for n being natural number st n >= 2 & dom fs = n holds
ex fs1 being FinSequence st
( len fs1 = n - 1 & ( for p being natural number st p >= 1 & p <= n - 1 holds
ex m1, m2 being non zero natural number ex f1 being Function of (free_magma (X,m1)),M ex f2 being Function of (free_magma (X,m2)),M st
( m1 = p & m2 = n - p & f1 = fs . m1 & f2 = fs . m2 & fs1 . p = [:f1,f2:] ) ) & Union fs1 = Union fs1 ) ) )
thus ( ( dom fs = 0 implies Union fs1 = {} ) & ( dom fs = 1 implies Union fs1 = f ) ) by A11; :: thesis: for n being natural number st n >= 2 & dom fs = n holds
ex fs1 being FinSequence st
( len fs1 = n - 1 & ( for p being natural number st p >= 1 & p <= n - 1 holds
ex m1, m2 being non zero natural number ex f1 being Function of (free_magma (X,m1)),M ex f2 being Function of (free_magma (X,m2)),M st
( m1 = p & m2 = n - p & f1 = fs . m1 & f2 = fs . m2 & fs1 . p = [:f1,f2:] ) ) & Union fs1 = Union fs1 )
thus for n being natural number st n >= 2 & dom fs = n holds
ex fs1 being FinSequence st
( len fs1 = n - 1 & ( for p being natural number st p >= 1 & p <= n - 1 holds
ex m1, m2 being non zero natural number ex f1 being Function of (free_magma (X,m1)),M ex f2 being Function of (free_magma (X,m2)),M st
( m1 = p & m2 = n - p & f1 = fs . m1 & f2 = fs . m2 & fs1 . p = [:f1,f2:] ) ) & Union fs1 = Union fs1 ) :: thesis: verum
proof
let n99 be natural number ; :: thesis: ( n99 >= 2 & dom fs = n99 implies ex fs1 being FinSequence st
( len fs1 = n99 - 1 & ( for p being natural number st p >= 1 & p <= n99 - 1 holds
ex m1, m2 being non zero natural number ex f1 being Function of (free_magma (X,m1)),M ex f2 being Function of (free_magma (X,m2)),M st
( m1 = p & m2 = n99 - p & f1 = fs . m1 & f2 = fs . m2 & fs1 . p = [:f1,f2:] ) ) & Union fs1 = Union fs1 ) )
assume n99 >= 2 ; :: thesis: ( not dom fs = n99 or ex fs1 being FinSequence st
( len fs1 = n99 - 1 & ( for p being natural number st p >= 1 & p <= n99 - 1 holds
ex m1, m2 being non zero natural number ex f1 being Function of (free_magma (X,m1)),M ex f2 being Function of (free_magma (X,m2)),M st
( m1 = p & m2 = n99 - p & f1 = fs . m1 & f2 = fs . m2 & fs1 . p = [:f1,f2:] ) ) & Union fs1 = Union fs1 ) )
assume A20: dom fs = n99 ; :: thesis: ex fs1 being FinSequence st
( len fs1 = n99 - 1 & ( for p being natural number st p >= 1 & p <= n99 - 1 holds
ex m1, m2 being non zero natural number ex f1 being Function of (free_magma (X,m1)),M ex f2 being Function of (free_magma (X,m2)),M st
( m1 = p & m2 = n99 - p & f1 = fs . m1 & f2 = fs . m2 & fs1 . p = [:f1,f2:] ) ) & Union fs1 = Union fs1 )
take fs1 ; :: thesis: ( len fs1 = n99 - 1 & ( for p being natural number st p >= 1 & p <= n99 - 1 holds
ex m1, m2 being non zero natural number ex f1 being Function of (free_magma (X,m1)),M ex f2 being Function of (free_magma (X,m2)),M st
( m1 = p & m2 = n99 - p & f1 = fs . m1 & f2 = fs . m2 & fs1 . p = [:f1,f2:] ) ) & Union fs1 = Union fs1 )
thus len fs1 = n99 - 1 by A12, A20, A19, FINSEQ_1:def 3; :: thesis: ( ( for p being natural number st p >= 1 & p <= n99 - 1 holds
ex m1, m2 being non zero natural number ex f1 being Function of (free_magma (X,m1)),M ex f2 being Function of (free_magma (X,m2)),M st
( m1 = p & m2 = n99 - p & f1 = fs . m1 & f2 = fs . m2 & fs1 . p = [:f1,f2:] ) ) & Union fs1 = Union fs1 )
thus for p being natural number st p >= 1 & p <= n99 - 1 holds
ex m1, m2 being non zero natural number ex f1 being Function of (free_magma (X,m1)),M ex f2 being Function of (free_magma (X,m2)),M st
( m1 = p & m2 = n99 - p & f1 = fs . m1 & f2 = fs . m2 & fs1 . p = [:f1,f2:] ) :: thesis: Union fs1 = Union fs1
proof
let p be natural number ; :: thesis: ( p >= 1 & p <= n99 - 1 implies ex m1, m2 being non zero natural number ex f1 being Function of (free_magma (X,m1)),M ex f2 being Function of (free_magma (X,m2)),M st
( m1 = p & m2 = n99 - p & f1 = fs . m1 & f2 = fs . m2 & fs1 . p = [:f1,f2:] ) )
assume A21: p >= 1 ; :: thesis: ( not p <= n99 - 1 or ex m1, m2 being non zero natural number ex f1 being Function of (free_magma (X,m1)),M ex f2 being Function of (free_magma (X,m2)),M st
( m1 = p & m2 = n99 - p & f1 = fs . m1 & f2 = fs . m2 & fs1 . p = [:f1,f2:] ) )
assume A22: p <= n99 - 1 ; :: thesis: ex m1, m2 being non zero natural number ex f1 being Function of (free_magma (X,m1)),M ex f2 being Function of (free_magma (X,m2)),M st
( m1 = p & m2 = n99 - p & f1 = fs . m1 & f2 = fs . m2 & fs1 . p = [:f1,f2:] )
then A23: p <= n9 by A20, XREAL_0:def 2;
p + 1 <= (n - 1) + 1 by A20, A22, XREAL_1:7;
then A24: (p + 1) - p <= n - p by XREAL_1:9;
then A25: n -' p = n - p by XREAL_0:def 2;
reconsider m1 = p as non zero natural number by A21;
reconsider m2 = n - p as non zero natural number by A24, A25;
p in Seg n9 by A21, A23, FINSEQ_1:1;
then reconsider f1 = fs . m1 as Function of (free_magma (X,m1)),M by A7, A13, A12;
- 1 >= - p by A21, XREAL_1:24;
then (- 1) + n >= (- p) + n by XREAL_1:7;
then m2 in Seg n9 by A12, A24, FINSEQ_1:1;
then reconsider f2 = fs . m2 as Function of (free_magma (X,m2)),M by A13, A7, A12;
take m1 ; :: thesis: ex m2 being non zero natural number ex f1 being Function of (free_magma (X,m1)),M ex f2 being Function of (free_magma (X,m2)),M st
( m1 = p & m2 = n99 - p & f1 = fs . m1 & f2 = fs . m2 & fs1 . p = [:f1,f2:] )
take m2 ; :: thesis: ex f1 being Function of (free_magma (X,m1)),M ex f2 being Function of (free_magma (X,m2)),M st
( m1 = p & m2 = n99 - p & f1 = fs . m1 & f2 = fs . m2 & fs1 . p = [:f1,f2:] )
take f1 ; :: thesis: ex f2 being Function of (free_magma (X,m2)),M st
( m1 = p & m2 = n99 - p & f1 = fs . m1 & f2 = fs . m2 & fs1 . p = [:f1,f2:] )
take f2 ; :: thesis: ( m1 = p & m2 = n99 - p & f1 = fs . m1 & f2 = fs . m2 & fs1 . p = [:f1,f2:] )
p in Seg n9 by A21, A23, FINSEQ_1:1;
then A26: ex m1, m2 being non zero natural number ex f1 being Function of (free_magma (X,m1)),M ex f2 being Function of (free_magma (X,m2)),M st
( m1 = p & m2 = n - p & f1 = fs . m1 & f2 = fs . m2 & fs1 . p = [:f1,f2:] ) by A19, A20, A21, A22;
thus ( m1 = p & m2 = n99 - p & f1 = fs . m1 & f2 = fs . m2 ) by A20; :: thesis: fs1 . p = [:f1,f2:]
thus fs1 . p = [:f1,f2:] by A26; :: thesis: verum
end;
thus Union fs1 = Union fs1 ; :: thesis: verum
end;
end;
hence S2[e, Union fs1] by A7; :: thesis: verum
end;
end;
end;
suppose A27: ex m being non zero natural number st
( m in dom fs & fs . m is not Function of (free_magma (X,m)),M ) ; :: thesis: ex u being set st S2[e,u]
take f ; :: thesis: S2[e,f]
thus S2[e,f] by A27; :: thesis: verum
end;
end;
end;
consider F2 being Function such that
A28: ( dom F2 = X1 ^omega & ( for e being set st e in X1 ^omega holds
S2[e,F2 . e] ) ) from CLASSES1:sch 1(A6);
 A29: for n being natural number
for fs being XFinSequence of st n >= 2 & dom fs = n & ( for m being non zero natural number st m in dom fs holds
fs . m is Function of (free_magma (X,m)),M ) & ex fs1 being FinSequence st
( len fs1 = n - 1 & ( for p being natural number st p >= 1 & p <= n - 1 holds
ex m1, m2 being non zero natural number ex f1 being Function of (free_magma (X,m1)),M ex f2 being 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 natural number ; :: thesis: for fs being XFinSequence of st n >= 2 & dom fs = n & ( for m being non zero natural number st m in dom fs holds
fs . m is Function of (free_magma (X,m)),M ) & ex fs1 being FinSequence st
( len fs1 = n - 1 & ( for p being natural number st p >= 1 & p <= n - 1 holds
ex m1, m2 being non zero natural number ex f1 being Function of (free_magma (X,m1)),M ex f2 being 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)
let fs be XFinSequence of ; :: thesis: ( n >= 2 & dom fs = n & ( for m being non zero natural number st m in dom fs holds
fs . m is Function of (free_magma (X,m)),M ) & ex fs1 being FinSequence st
( len fs1 = n - 1 & ( for p being natural number st p >= 1 & p <= n - 1 holds
ex m1, m2 being non zero natural number ex f1 being Function of (free_magma (X,m1)),M ex f2 being 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 ) implies F2 . fs in Funcs ((free_magma (X,n)), the carrier of M) )
assume A30: n >= 2 ; :: thesis: ( not dom fs = n or ex m being non zero natural number st
( m in dom fs & fs . m is not Function of (free_magma (X,m)),M ) or for fs1 being FinSequence holds
( not len fs1 = n - 1 or ex p being natural number st
( p >= 1 & p <= n - 1 & ( for m1, m2 being non zero natural number
for f1 being Function of (free_magma (X,m1)),M
for f2 being Function of (free_magma (X,m2)),M holds
( not m1 = p or not m2 = n - p or not f1 = fs . m1 or not f2 = fs . m2 or not fs1 . p = [:f1,f2:] ) ) ) or not F2 . fs = Union fs1 ) or F2 . fs in Funcs ((free_magma (X,n)), the carrier of M) )
assume dom fs = n ; :: thesis: ( ex m being non zero natural number st
( m in dom fs & fs . m is not Function of (free_magma (X,m)),M ) or for fs1 being FinSequence holds
( not len fs1 = n - 1 or ex p being natural number st
( p >= 1 & p <= n - 1 & ( for m1, m2 being non zero natural number
for f1 being Function of (free_magma (X,m1)),M
for f2 being Function of (free_magma (X,m2)),M holds
( not m1 = p or not m2 = n - p or not f1 = fs . m1 or not f2 = fs . m2 or not fs1 . p = [:f1,f2:] ) ) ) or not F2 . fs = Union fs1 ) or F2 . fs in Funcs ((free_magma (X,n)), the carrier of M) )
assume for m being non zero natural number st m in dom fs holds
fs . m is Function of (free_magma (X,m)),M ; :: thesis: ( for fs1 being FinSequence holds
( not len fs1 = n - 1 or ex p being natural number st
( p >= 1 & p <= n - 1 & ( for m1, m2 being non zero natural number
for f1 being Function of (free_magma (X,m1)),M
for f2 being Function of (free_magma (X,m2)),M holds
( not m1 = p or not m2 = n - p or not f1 = fs . m1 or not f2 = fs . m2 or not fs1 . p = [:f1,f2:] ) ) ) or not F2 . fs = Union fs1 ) or F2 . fs in Funcs ((free_magma (X,n)), the carrier of M) )
assume ex fs1 being FinSequence st
( len fs1 = n - 1 & ( for p being natural number st p >= 1 & p <= n - 1 holds
ex m1, m2 being non zero natural number ex f1 being Function of (free_magma (X,m1)),M ex f2 being 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 ) ; :: thesis: F2 . fs in Funcs ((free_magma (X,n)), the carrier of M)
then consider fs1 being FinSequence such that
A31: len fs1 = n - 1 and
A32: for p being natural number st p >= 1 & p <= n - 1 holds
ex m1, m2 being non zero natural number ex f1 being Function of (free_magma (X,m1)),M ex f2 being Function of (free_magma (X,m2)),M st
( m1 = p & m2 = n - p & f1 = fs . m1 & f2 = fs . m2 & fs1 . p = [:f1,f2:] ) and
A33: F2 . fs = Union fs1 ;
A34: for x being set st x in F2 . fs holds
ex y, z being set st x = [y,z]
proof
let x be set ; :: thesis: ( x in F2 . fs implies ex y, z being set st x = [y,z] )
assume x in F2 . fs ; :: thesis: ex y, z being set st x = [y,z]
then x in union (rng fs1) by A33, CARD_3:def 4;
then consider Y being set such that
A35: ( x in Y & Y in rng fs1 ) by TARSKI:def 4;
consider p being set such that
A36: ( p in dom fs1 & Y = fs1 . p ) by A35, FUNCT_1:def 3;
reconsider p = p as natural number by A36;
p in Seg (len fs1) by A36, FINSEQ_1:def 3;
then ( 1 <= p & p <= n - 1 ) by A31, FINSEQ_1:1;
then consider m1, m2 being non zero natural number , f1 being Function of (free_magma (X,m1)),M, f2 being Function of (free_magma (X,m2)),M such that
A37: ( m1 = p & m2 = n - p & f1 = fs . m1 & f2 = fs . m2 & fs1 . p = [:f1,f2:] ) by A32;
consider y, z being set such that
A38: x = [y,z] by A35, A36, A37, RELAT_1:def 1;
take y ; :: thesis: ex z being set st x = [y,z]
take z ; :: thesis: x = [y,z]
thus x = [y,z] by A38; :: thesis: verum
end;
for x, y1, y2 being set st [x,y1] in F2 . fs & [x,y2] in F2 . fs holds
y1 = y2
proof
let x, y1, y2 be set ; :: thesis: ( [x,y1] in F2 . fs & [x,y2] in F2 . fs implies y1 = y2 )
assume [x,y1] in F2 . fs ; :: thesis: ( not [x,y2] in F2 . fs or y1 = y2 )
then [x,y1] in union (rng fs1) by A33, CARD_3:def 4;
then consider Y1 being set such that
A39: ( [x,y1] in Y1 & Y1 in rng fs1 ) by TARSKI:def 4;
consider p1 being set such that
A40: ( p1 in dom fs1 & Y1 = fs1 . p1 ) by A39, FUNCT_1:def 3;
reconsider p1 = p1 as natural number by A40;
p1 in Seg (len fs1) by A40, FINSEQ_1:def 3;
then ( 1 <= p1 & p1 <= n - 1 ) by A31, FINSEQ_1:1;
then consider m19, m29 being non zero natural number , f19 being Function of (free_magma (X,m19)),M, f29 being Function of (free_magma (X,m29)),M such that
A41: ( m19 = p1 & m29 = n - p1 & f19 = fs . m19 & f29 = fs . m29 & fs1 . p1 = [:f19,f29:] ) by A32;
A42: x in dom [:f19,f29:] by A39, A40, A41, FUNCT_1:1;
then x `2 in {m19} by MCART_1:10;
then A43: x `2 = m19 by TARSKI:def 1;
assume [x,y2] in F2 . fs ; :: thesis: y1 = y2
then [x,y2] in union (rng fs1) by A33, CARD_3:def 4;
then consider Y2 being set such that
A44: ( [x,y2] in Y2 & Y2 in rng fs1 ) by TARSKI:def 4;
consider p2 being set such that
A45: ( p2 in dom fs1 & Y2 = fs1 . p2 ) by A44, FUNCT_1:def 3;
reconsider p2 = p2 as natural number by A45;
p2 in Seg (len fs1) by A45, FINSEQ_1:def 3;
then ( 1 <= p2 & p2 <= n - 1 ) by A31, FINSEQ_1:1;
then consider m199, m299 being non zero natural number , f199 being Function of (free_magma (X,m199)),M, f299 being Function of (free_magma (X,m299)),M such that
A46: ( m199 = p2 & m299 = n - p2 & f199 = fs . m199 & f299 = fs . m299 & fs1 . p2 = [:f199,f299:] ) by A32;
A47: x in dom [:f199,f299:] by A44, A45, A46, FUNCT_1:1;
then x `2 in {m199} by MCART_1:10;
then A48: ( f19 = f199 & f29 = f299 ) by A41, A46, A43, TARSKI:def 1;
A49: x `1 in [:(free_magma (X,m19)),(free_magma (X,m29)):] by A42, MCART_1:10;
reconsider x1 = x as Element of [:[:(free_magma (X,m19)),(free_magma (X,m29)):],{m19}:] by A42;
reconsider y19 = (x `1) `1 as Element of free_magma (X,m19) by A49, MCART_1:10;
reconsider z1 = (x `1) `2 as Element of free_magma (X,m29) by A49, MCART_1:10;
A50: x `1 in [:(free_magma (X,m199)),(free_magma (X,m299)):] by A47, MCART_1:10;
reconsider x2 = x as Element of [:[:(free_magma (X,m199)),(free_magma (X,m299)):],{m199}:] by A47;
reconsider y29 = (x `1) `1 as Element of free_magma (X,m199) by A50, MCART_1:10;
reconsider z2 = (x `1) `2 as Element of free_magma (X,m299) by A50, MCART_1:10;
thus y1 = [:f19,f29:] . x1 by A39, A40, A41, FUNCT_1:1
.= (f19 . y19) * (f29 . z1) by Def20
.= (f199 . y29) * (f299 . z2) by A48
.= [:f199,f299:] . x2 by Def20
.= y2 by A44, A45, A46, FUNCT_1:1 ; :: thesis: verum
end;
then reconsider f9 = F2 . fs as Function by A34, FUNCT_1:def 1, RELAT_1:def 1;
for x being set holds
( x in free_magma (X,n) iff ex y being set st [x,y] in f9 )
proof
let x be set ; :: thesis: ( x in free_magma (X,n) iff ex y being set st [x,y] in f9 )
hereby :: thesis: ( ex y being set st [x,y] in f9 implies x in free_magma (X,n) )
assume x in free_magma (X,n) ; :: thesis: ex y being set st [x,y] in f9
then consider p, m being natural number such that
A51: ( 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 A30, Th21;
consider m1, m2 being non zero natural number , f1 being Function of (free_magma (X,m1)),M, f2 being Function of (free_magma (X,m2)),M such that
A52: ( m1 = p & m2 = n - p & f1 = fs . m1 & f2 = fs . m2 & fs1 . p = [:f1,f2:] ) by A32, A51;
reconsider x9 = x as Element of [:[:(free_magma (X,m1)),(free_magma (X,m2)):],{m1}:] by A51, A52;
reconsider y9 = (x `1) `1 as Element of free_magma (X,m1) by A51, A52;
reconsider z9 = (x `1) `2 as Element of free_magma (X,m2) by A51, A52;
reconsider y = (f1 . y9) * (f2 . z9) as set ;
A53: dom [:f1,f2:] = [:[:(free_magma (X,m1)),(free_magma (X,m2)):],{m1}:] by FUNCT_2:def 1;
A54: [:f1,f2:] . x9 = y by Def20;
take y = y; :: thesis: [x,y] in f9
A55: [x,y] in fs1 . p by A52, A53, A54, FUNCT_1:1;
p in Seg (len fs1) by A51, A31, 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 A55, TARSKI:def 4;
hence [x,y] in f9 by A33, CARD_3:def 4; :: thesis: verum
end;
given y being set such that A56: [x,y] in f9 ; :: thesis: x in free_magma (X,n)
[x,y] in union (rng fs1) by A33, A56, CARD_3:def 4;
then consider Y being set such that
A57: ( [x,y] in Y & Y in rng fs1 ) by TARSKI:def 4;
consider p being set such that
A58: ( p in dom fs1 & Y = fs1 . p ) by A57, FUNCT_1:def 3;
A59: p in Seg (len fs1) by A58, FINSEQ_1:def 3;
reconsider p = p as natural number by A58;
( p >= 1 & p <= n - 1 ) by A59, A31, FINSEQ_1:1;
then consider m1, m2 being non zero natural number , f1 being Function of (free_magma (X,m1)),M, f2 being Function of (free_magma (X,m2)),M such that
A60: ( m1 = p & m2 = n - p & f1 = fs . m1 & f2 = fs . m2 & fs1 . p = [:f1,f2:] ) by A32;
A61: x in dom [:f1,f2:] by A57, A58, A60, FUNCT_1:1;
then A62: ( x `1 in [:(free_magma (X,m1)),(free_magma (X,m2)):] & x `2 in {m1} ) by MCART_1:10;
then A63: ( (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 A61, MCART_1:21;
then A64: x = [[((x `1) `1),((x `1) `2)],(x `2)] by A62, MCART_1:21;
x `2 = m1 by A62, TARSKI:def 1;
then x in free_magma (X,(m1 + m2)) by A64, Th22, A63;
hence x in free_magma (X,n) by A60; :: thesis: verum
end;
then A65: dom f9 = free_magma (X,n) by RELAT_1:def 4;
for y being set st y in rng f9 holds
y in the carrier of M
proof
let y be set ; :: thesis: ( y in rng f9 implies y in the carrier of M )
assume y in rng f9 ; :: thesis: y in the carrier of M
then consider x being set such that
A66: ( x in dom f9 & y = f9 . x ) by FUNCT_1:def 3;
[x,y] in Union fs1 by A33, A66, FUNCT_1:1;
then [x,y] in union (rng fs1) by CARD_3:def 4;
then consider Y being set such that
A67: ( [x,y] in Y & Y in rng fs1 ) by TARSKI:def 4;
consider p being set such that
A68: ( p in dom fs1 & Y = fs1 . p ) by A67, FUNCT_1:def 3;
A69: p in Seg (len fs1) by A68, FINSEQ_1:def 3;
reconsider p = p as natural number by A68;
( p >= 1 & p <= n - 1 ) by A69, A31, FINSEQ_1:1;
then consider m1, m2 being non zero natural number , f1 being Function of (free_magma (X,m1)),M, f2 being Function of (free_magma (X,m2)),M such that
A70: ( m1 = p & m2 = n - p & f1 = fs . m1 & f2 = fs . m2 & fs1 . p = [:f1,f2:] ) by A32;
y in rng [:f1,f2:] by A67, A68, A70, RELAT_1:def 5;
hence y in the carrier of M ; :: thesis: verum
end;
then rng f9 c= the carrier of M by TARSKI:def 3;
hence F2 . fs in Funcs ((free_magma (X,n)), the carrier of M) by A65, FUNCT_2:def 2; :: thesis: verum
end;
for e being set st e in X1 ^omega holds
F2 . e in X1
proof
let e be set ; :: thesis: ( e in X1 ^omega implies F2 . e in X1 )
assume A71: e in X1 ^omega ; :: thesis: F2 . e in X1
then reconsider fs = e as XFinSequence of by AFINSQ_1:def 7;
per cases ( for m being non zero natural number st m in dom fs holds
fs . m is Function of (free_magma (X,m)),M or ex m being non zero natural number st
( m in dom fs & fs . m is not Function of (free_magma (X,m)),M ) ) ;
suppose A72: for m being non zero natural number st m in dom fs holds
fs . m is Function of (free_magma (X,m)),M ; :: thesis: F2 . e in X1
then A73: ( ( dom fs = 0 implies F2 . e = {} ) & ( dom fs = 1 implies F2 . e = f ) & ( for n being natural number st n >= 2 & dom fs = n holds
ex fs1 being FinSequence st
( len fs1 = n - 1 & ( for p being natural number st p >= 1 & p <= n - 1 holds
ex m1, m2 being non zero natural number ex f1 being Function of (free_magma (X,m1)),M ex f2 being 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 A71, A28;
( 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 A74: ( dom fs = 0 or dom fs = 1 or (dom fs) + 1 > 1 + 1 ) by XREAL_1:6;
per cases ( dom fs = 0 or dom fs = 1 or dom fs >= 2 ) by A74, NAT_1:13;
suppose A75: dom fs = 0 ; :: thesis: F2 . e in X1
Funcs ({}, the carrier of M) = {{}} by FUNCT_5:57;
then A76: {} in Funcs ({}, the carrier of M) by TARSKI:def 1;
S1[ 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 A76, TARSKI:def 4;
hence F2 . e in X1 by A75, A73, CARD_3:def 4; :: thesis: verum
end;
suppose dom fs = 1 ; :: thesis: F2 . e in X1
hence F2 . e in X1 by A5, A72, A71, A28; :: thesis: verum
end;
suppose A77: dom fs >= 2 ; :: thesis: F2 . e in X1
set n = dom fs;
ex fs1 being FinSequence st
( len fs1 = (dom fs) - 1 & ( for p being natural number st p >= 1 & p <= (dom fs) - 1 holds
ex m1, m2 being non zero natural number ex f1 being Function of (free_magma (X,m1)),M ex f2 being Function of (free_magma (X,m2)),M st
( m1 = p & m2 = (dom fs) - p & f1 = fs . m1 & f2 = fs . m2 & fs1 . p = [:f1,f2:] ) ) & F2 . e = Union fs1 ) by A72, A77, A71, A28;
then A78: F2 . e in Funcs ((free_magma (X,(dom fs))), the carrier of M) by A29, A77, A72;
A79: dom fs in dom F1 by A2, ORDINAL1:def 12;
then S1[ dom fs,F1 . (dom fs)] by A2;
then Funcs ((free_magma (X,(dom fs))), the carrier of M) in rng F1 by A79, FUNCT_1:3;
then F2 . e in union (rng F1) by A78, TARSKI:def 4;
hence F2 . e in X1 by CARD_3:def 4; :: thesis: verum
end;
end;
end;
suppose ex m being non zero natural number st
( m in dom fs & fs . m is not Function of (free_magma (X,m)),M ) ; :: thesis: F2 . e in X1
hence F2 . e in X1 by A5, A71, A28; :: thesis: verum
end;
end;
end;
then reconsider F2 = F2 as Function of (X1 ^omega),X1 by A28, FUNCT_2:3;
deffunc H1( XFinSequence of ) -> Element of X1 = F2 . $1;
consider F3 being Function of NAT,X1 such that
A80: for n being natural number holds F3 . n = H1(F3 | n) from ALGSTR_4:sch 4();
 A81: for n being natural number st n > 0 holds
F3 . n is Function of (free_magma (X,n)),M
proof
defpred S3[ Nat] means for n being natural number st $1 = n & n > 0 holds
F3 . n is Function of (free_magma (X,n)),M;
A82: for k being Nat st ( for n being Nat st n < k holds
S3[n] ) holds
S3[k]
proof
let k be Nat; :: thesis: ( ( for n being Nat st n < k holds
S3[n] ) implies S3[k] )
assume A83: for n being Nat st n < k holds
S3[n] ; :: thesis: S3[k]
thus S3[k] :: thesis: verum
proof
let n be natural number ; :: thesis: ( k = n & n > 0 implies F3 . n is Function of (free_magma (X,n)),M )
assume A84: k = n ; :: thesis: ( not n > 0 or F3 . n is Function of (free_magma (X,n)),M )
assume n > 0 ; :: thesis: F3 . n is Function of (free_magma (X,n)),M
A85: for m being non zero natural number st m in dom (F3 | n) holds
(F3 | n) . m is Function of (free_magma (X,m)),M
proof
let m be non zero natural number ; :: thesis: ( m in dom (F3 | n) implies (F3 | n) . m is Function of (free_magma (X,m)),M )
assume A86: m in dom (F3 | n) ; :: thesis: (F3 | n) . m is Function of (free_magma (X,m)),M
then A87: (F3 | n) . m = F3 . m by FUNCT_1:47;
m in k by A84, A86, RELAT_1:57;
then m < k by NAT_1:44;
hence (F3 | n) . m is Function of (free_magma (X,m)),M by A87, A83; :: thesis: verum
end;
A88: F3 | n in X1 ^omega by AFINSQ_1:def 7;
reconsider fs = F3 | n as XFinSequence of ;
A89: ( ( dom fs = 0 implies F2 . fs = {} ) & ( dom fs = 1 implies F2 . fs = f ) & ( for n being natural number st n >= 2 & dom fs = n holds
ex fs1 being FinSequence st
( len fs1 = n - 1 & ( for p being natural number st p >= 1 & p <= n - 1 holds
ex m1, m2 being non zero natural number ex f1 being Function of (free_magma (X,m1)),M ex f2 being 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 A85, A88, A28;
A90: n in NAT by ORDINAL1:def 12;
dom F3 = NAT by FUNCT_2:def 1;
then A91: n c= dom F3 by A90, ORDINAL1:def 2;
A92: dom fs = (dom F3) /\ n by RELAT_1:61
.= n by A91, 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 A93: ( n = 0 or n = 1 or n + 1 > 1 + 1 ) by XREAL_1:6;
per cases ( n = 0 or n = 1 or n >= 2 ) by A93, NAT_1:13;
suppose A94: n = 0 ; :: thesis: F2 . fs is Function of (free_magma (X,n)),M
Funcs ({}, the carrier of M) = {{}} by FUNCT_5:57;
then F2 . fs in Funcs ({}, the carrier of M) by A94, A89, TARSKI:def 1;
then F2 . fs in Funcs ((free_magma (X,n)), the carrier of M) by A94, Def13;
then ex f being Function st
( F2 . fs = f & dom f = free_magma (X,n) & rng f c= the carrier of M ) by FUNCT_2:def 2;
hence F2 . fs is Function of (free_magma (X,n)),M by FUNCT_2:2; :: thesis: verum
end;
suppose A95: n = 1 ; :: thesis: F2 . fs is Function of (free_magma (X,n)),M
free_magma (X,1) = X by Def13;
hence F2 . fs is Function of (free_magma (X,n)),M by A85, A88, A28, A95, A92; :: thesis: verum
end;
suppose A96: n >= 2 ; :: thesis: F2 . fs is Function of (free_magma (X,n)),M
then ex fs1 being FinSequence st
( len fs1 = n - 1 & ( for p being natural number st p >= 1 & p <= n - 1 holds
ex m1, m2 being non zero natural number ex f1 being Function of (free_magma (X,m1)),M ex f2 being 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 A85, A88, A28, A92;
then F2 . fs in Funcs ((free_magma (X,n)), the carrier of M) by A29, A96, A92, A85;
then ex f being Function st
( F2 . fs = f & dom f = free_magma (X,n) & rng f c= the carrier of M ) by FUNCT_2:def 2;
hence F2 . fs is Function of (free_magma (X,n)),M by FUNCT_2:2; :: thesis: verum
end;
end;
end;
hence F3 . n is Function of (free_magma (X,n)),M by A80; :: thesis: verum
end;
end;
for k being Nat holds S3[k] from NAT_1:sch 4(A82);
 hence for n being natural number st n > 0 holds
F3 . n is Function of (free_magma (X,n)),M ; :: thesis: verum
end;
reconsider X9 = the carrier of (free_magma X) as set ;
defpred S3[ set , set ] means for w being Element of (free_magma X)
for f9 being Function of (free_magma (X,(w `2))),M st w = $1 & f9 = F3 . (w `2) holds
$2 = f9 . (w `1);
A97: for x being set st x in X9 holds
ex y being set st
( y in the carrier of M & S3[x,y] )
proof
let x be set ; :: thesis: ( x in X9 implies ex y being set st
( y in the carrier of M & S3[x,y] ) )
assume x in X9 ; :: thesis: ex y being set st
( y in the carrier of M & S3[x,y] )
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 A81;
set y = f9 . (w `1);
take f9 . (w `1) ; :: thesis: ( f9 . (w `1) in the carrier of M & S3[x,f9 . (w `1)] )
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 f9 . (w `1) in the carrier of M by FUNCT_2:5; :: thesis: S3[x,f9 . (w `1)]
thus S3[x,f9 . (w `1)] ; :: thesis: verum
end;
consider h being Function of X9, the carrier of M such that
A98: for x being set st x in X9 holds
S3[x,h . x] from FUNCT_2:sch 1(A97);
 reconsider h = h as Function of (free_magma X),M ;
take h ; :: thesis: ( h is multiplicative & h extends f * ((canon_image (X,1)) ") )
for a, b being Element of (free_magma X) holds h . (a * b) = (h . a) * (h . b)
proof
let a, b be Element of (free_magma X); :: thesis: h . (a * b) = (h . a) * (h . b)
reconsider fab = F3 . ((a * b) `2) as Function of (free_magma (X,((a * b) `2))),M by A81;
a * b = [[[(a `1),(b `1)],(a `2)],((length a) + (length b))] by Th31;
then A99: ( (a * b) `1 = [[(a `1),(b `1)],(a `2)] & (a * b) `2 = (length a) + (length b) ) by MCART_1:7;
then A100: fab = F2 . (F3 | ((length a) + (length b))) by A80;
A101: F3 | ((length a) + (length b)) in X1 ^omega by AFINSQ_1:def 7;
A102: for m being non zero natural number 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 natural number ; :: thesis: ( m in dom (F3 | ((length a) + (length b))) implies (F3 | ((length a) + (length b))) . m is Function of (free_magma (X,m)),M )
assume A103: m in dom (F3 | ((length a) + (length b))) ; :: thesis: (F3 | ((length a) + (length b))) . m is Function of (free_magma (X,m)),M
F3 . m is Function of (free_magma (X,m)),M by A81;
hence (F3 | ((length a) + (length b))) . m is Function of (free_magma (X,m)),M by A103, FUNCT_1:47; :: thesis: verum
end;
set n = (length a) + (length b);
( length a >= 1 & length b >= 1 ) by Th32;
then A104: (length a) + (length b) >= 1 + 1 by XREAL_1:7;
A105: (length a) + (length b) in NAT by ORDINAL1:def 12;
dom F3 = NAT by FUNCT_2:def 1;
then A106: (length a) + (length b) c= dom F3 by A105, ORDINAL1:def 2;
dom (F3 | ((length a) + (length b))) = (dom F3) /\ ((length a) + (length b)) by RELAT_1:61
.= (length a) + (length b) by A106, XBOOLE_1:28 ;
then consider fs1 being FinSequence such that
A107: len fs1 = ((length a) + (length b)) - 1 and
A108: for p being natural number st p >= 1 & p <= ((length a) + (length b)) - 1 holds
ex m1, m2 being non zero natural number ex f1 being Function of (free_magma (X,m1)),M ex f2 being Function of (free_magma (X,m2)),M st
( m1 = p & m2 = ((length a) + (length b)) - p & f1 = (F3 | ((length a) + (length b))) . m1 & f2 = (F3 | ((length a) + (length b))) . m2 & fs1 . p = [:f1,f2:] ) and
A109: fab = Union fs1 by A102, A104, A101, A28, A100;
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 A109, FUNCT_1:1;
then [((a * b) `1),(fab . ((a * b) `1))] in union (rng fs1) by CARD_3:def 4;
then consider Y being set such that
A110: ( [((a * b) `1),(fab . ((a * b) `1))] in Y & Y in rng fs1 ) by TARSKI:def 4;
consider p being set such that
A111: ( p in dom fs1 & Y = fs1 . p ) by A110, FUNCT_1:def 3;
A112: p in Seg (len fs1) by A111, FINSEQ_1:def 3;
reconsider p = p as natural number by A111;
( p >= 1 & p <= ((length a) + (length b)) - 1 ) by A112, A107, FINSEQ_1:1;
then consider m1, m2 being non zero natural number , f1 being Function of (free_magma (X,m1)),M, f2 being Function of (free_magma (X,m2)),M such that
A113: ( m1 = p & m2 = ((length a) + (length b)) - p & f1 = (F3 | ((length a) + (length b))) . m1 & f2 = (F3 | ((length a) + (length b))) . m2 & fs1 . p = [:f1,f2:] ) by A108;
A114: (a * b) `1 in dom [:f1,f2:] by A113, A110, A111, 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 A115: ( [(a `1),(b `1)] in [:(free_magma (X,m1)),(free_magma (X,m2)):] & a `2 in {m1} ) by A99, MCART_1:7;
then m1 = a `2 by TARSKI:def 1;
then A116: m1 = length a by Def18;
length b >= 0 + 1 by Th32;
then (length b) + (length a) > 0 + (length a) by XREAL_1:6;
then A117: m1 in (length a) + (length b) by A116, NAT_1:44;
length a >= 0 + 1 by Th32;
then (length a) + (length b) > 0 + (length b) by XREAL_1:6;
then A118: m2 in (length a) + (length b) by A116, A113, NAT_1:44;
reconsider x = (a * b) `1 as Element of [:[:(free_magma (X,m1)),(free_magma (X,m2)):],{m1}:] by A114;
A119: 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 A119, MCART_1:10;
A120: x `1 = [(a `1),(b `1)] by A99, MCART_1:7;
A121: [:f1,f2:] . x = (f1 . y) * (f2 . z) by Def20;
A122: h . (a * b) = fab . ((a * b) `1) by A98;
A123: fab . ((a * b) `1) = [:f1,f2:] . x by A113, A110, A111, FUNCT_1:1;
reconsider fa = F3 . (a `2) as Function of (free_magma (X,(a `2))),M by A81;
reconsider fb = F3 . (b `2) as Function of (free_magma (X,(b `2))),M by A81;
f1 = F3 . m1 by A113, A117, FUNCT_1:49
.= fa by A115, TARSKI:def 1 ;
then A124: fa . (a `1) = f1 . y by A120, MCART_1:7;
f2 = F3 . m2 by A113, A118, FUNCT_1:49
.= fb by Def18, A116, A113 ;
then A125: fb . (b `1) = f2 . z by A120, MCART_1:7;
h . b = fb . (b `1) by A98;
hence h . (a * b) = (h . a) * (h . b) by A121, A122, A124, A125, A98, A123; :: thesis: verum
end;
hence h is multiplicative by GROUP_6:def 6; :: thesis: h extends f * ((canon_image (X,1)) ")
set fX = canon_image (X,1);
for x being set st x in dom (f * ((canon_image (X,1)) ")) holds
x in dom h
proof
let x be set ; :: thesis: ( x in dom (f * ((canon_image (X,1)) ")) implies x in dom h )
assume A126: x in dom (f * ((canon_image (X,1)) ")) ; :: thesis: x in dom h
dom (f * ((canon_image (X,1)) ")) c= dom ((canon_image (X,1)) ") by RELAT_1:25;
then x in dom ((canon_image (X,1)) ") by A126;
then x in rng (canon_image (X,1)) by FUNCT_1:33;
then x in the carrier of (free_magma X) ;
hence x in dom h by FUNCT_2:def 1; :: thesis: verum
end;
then A127: dom (f * ((canon_image (X,1)) ")) c= dom h by TARSKI:def 3;
for x being set st x in (dom h) /\ (dom (f * ((canon_image (X,1)) "))) holds
h . x = (f * ((canon_image (X,1)) ")) . x
proof
let x be set ; :: thesis: ( x in (dom h) /\ (dom (f * ((canon_image (X,1)) "))) implies h . x = (f * ((canon_image (X,1)) ")) . x )
assume x in (dom h) /\ (dom (f * ((canon_image (X,1)) "))) ; :: thesis: h . x = (f * ((canon_image (X,1)) ")) . x
then A128: x in dom (f * ((canon_image (X,1)) ")) by A127, XBOOLE_1:28;
A129: dom (f * ((canon_image (X,1)) ")) c= dom ((canon_image (X,1)) ") by RELAT_1:25;
then x in dom ((canon_image (X,1)) ") by A128;
then x in rng (canon_image (X,1)) by FUNCT_1:33;
then consider x9 being set such that
A130: ( x9 in dom (canon_image (X,1)) & x = (canon_image (X,1)) . x9 ) by FUNCT_1:def 3;
A131: 1 in {1} by TARSKI:def 1;
[:(free_magma (X,1)),{1}:] c= free_magma_carrier X by Lm1;
then A132: [:X,{1}:] c= free_magma_carrier X by Def13;
A133: x9 in X by A130, Lm3;
A134: x = [x9,1] by A130, Def19;
then x in [:X,{1}:] by A131, A133, ZFMISC_1:def 2;
then reconsider w = x as Element of (free_magma X) by A132;
A135: ((canon_image (X,1)) ") . x = x9 by A130, FUNCT_1:34;
set f9 = F3 . (w `2);
reconsider f9 = F3 . (w `2) as Function of (free_magma (X,(w `2))),M by A81;
A136: f9 = F3 . 1 by A134, MCART_1:7
.= H1(F3 | 1) by A80 ;
A137: for m being non zero natural number st m in dom (F3 | 1) holds
(F3 | 1) . m is Function of (free_magma (X,m)),M
proof
let m be non zero natural number ; :: thesis: ( m in dom (F3 | 1) implies (F3 | 1) . m is Function of (free_magma (X,m)),M )
assume m in dom (F3 | 1) ; :: thesis: (F3 | 1) . m is Function of (free_magma (X,m)),M
then (F3 | 1) . m = F3 . m by FUNCT_1:47;
hence (F3 | 1) . m is Function of (free_magma (X,m)),M by A81; :: thesis: verum
end;
A138: F3 | 1 in X1 ^omega by AFINSQ_1:def 7;
reconsider fs = F3 | 1 as XFinSequence of ;
dom F3 = NAT by FUNCT_2:def 1;
then A139: 1 c= dom F3 by ORDINAL1:def 2;
A140: dom fs = (dom F3) /\ 1 by RELAT_1:61
.= 1 by A139, XBOOLE_1:28 ;
thus h . x = f9 . (w `1) by A98
.= f9 . x9 by A134, MCART_1:7
.= f . (((canon_image (X,1)) ") . x) by A135, A136, A140, A137, A138, A28
.= (f * ((canon_image (X,1)) ")) . x by A129, A128, FUNCT_1:13 ; :: thesis: verum
end;
then h tolerates f * ((canon_image (X,1)) ") by PARTFUN1:def 4;
hence h extends f * ((canon_image (X,1)) ") by A127, Def2; :: thesis: verum