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[ object , object ] means ex n being Nat st
( n = $1 & $2 = Funcs ((free_magma (X,n)), the carrier of M) );
A1: for x being object st x in NAT holds
ex y being object st S1[x,y]
proof
let x be object ; :: thesis: ( x in NAT implies ex y being object st S1[x,y] )
assume x in NAT ; :: thesis: ex y being object st S1[x,y]
then reconsider n = x as Nat ;
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 object 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[ object , object ] means for fs being XFinSequence of X1 st $1 = fs holds
( ( ( for m being 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 being Nat st n >= 2 & dom fs = n holds
ex fs1 being FinSequence st
( len fs1 = n - 1 & ( for p being Nat st p >= 1 & p <= n - 1 holds
ex m1, m2 being non zero Nat 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 Nat st
( m in dom fs & fs . m is not Function of (free_magma (X,m)),M ) implies $2 = f ) );
A6: for e being object st e in X1 ^omega holds
ex u being object st S2[e,u]
proof
let e be object ; :: thesis: ( e in X1 ^omega implies ex u being object st S2[e,u] )
assume e in X1 ^omega ; :: thesis: ex u being object st S2[e,u]
then reconsider fs = e as XFinSequence of X1 by AFINSQ_1:def 7;
per cases ( for m being non zero Nat st m in dom fs holds
fs . m is Function of (free_magma (X,m)),M or ex m being non zero Nat st
( m in dom fs & fs . m is not Function of (free_magma (X,m)),M ) ) ;
suppose A7: for m being non zero Nat st m in dom fs holds
fs . m is Function of (free_magma (X,m)),M ; :: thesis: ex u being object 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 object 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 object 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 object st S2[e,u]
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 S3[ set , object ] means for p being Nat st p >= 1 & p <= n - 1 & $1 = p holds
ex m1, m2 being non zero Nat 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 object st S3[k,x]
proof
let k be Nat; :: thesis: ( k in Seg n9 implies ex x being object st S3[k,x] )
assume A15: k in Seg n9 ; :: thesis: ex x being object 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 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 [: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 :: thesis: ( ( for m being non zero Nat st m in dom fs holds
fs . m is Function of (free_magma (X,m)),M ) implies ( ( dom fs = 0 implies Union fs1 = {} ) & ( dom fs = 1 implies Union fs1 = f ) & ( for n being Nat st n >= 2 & dom fs = n holds
ex fs1 being FinSequence st
( len fs1 = n - 1 & ( for p being Nat st p >= 1 & p <= n - 1 holds
ex m1, m2 being non zero Nat 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 ) ) ) )
assume for m being non zero Nat 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 Nat st n >= 2 & dom fs = n holds
ex fs1 being FinSequence st
( len fs1 = n - 1 & ( for p being Nat st p >= 1 & p <= n - 1 holds
ex m1, m2 being non zero Nat 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 Nat st n >= 2 & dom fs = n holds
ex fs1 being FinSequence st
( len fs1 = n - 1 & ( for p being Nat st p >= 1 & p <= n - 1 holds
ex m1, m2 being non zero Nat 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 Nat st n >= 2 & dom fs = n holds
ex fs1 being FinSequence st
( len fs1 = n - 1 & ( for p being Nat st p >= 1 & p <= n - 1 holds
ex m1, m2 being non zero Nat 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 Nat; :: thesis: ( n99 >= 2 & dom fs = n99 implies ex fs1 being FinSequence st
( len fs1 = n99 - 1 & ( for p being Nat st p >= 1 & p <= n99 - 1 holds
ex m1, m2 being non zero Nat 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 Nat st p >= 1 & p <= n99 - 1 holds
ex m1, m2 being non zero Nat 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 Nat st p >= 1 & p <= n99 - 1 holds
ex m1, m2 being non zero Nat 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 Nat st p >= 1 & p <= n99 - 1 holds
ex m1, m2 being non zero Nat 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 Nat st p >= 1 & p <= n99 - 1 holds
ex m1, m2 being non zero Nat 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 Nat st p >= 1 & p <= n99 - 1 holds
ex m1, m2 being non zero Nat 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:] ) by A20, FINSEQ_1:1, A12, A19; :: thesis: Union fs1 = Union fs1
thus Union fs1 = Union fs1 ; :: thesis: verum
end;
end;
hence S2[e, Union fs1] by A7; :: thesis: verum
end;
end;
end;
suppose A21: ex m being non zero Nat st
( m in dom fs & fs . m is not Function of (free_magma (X,m)),M ) ; :: thesis: ex u being object st S2[e,u]
take f ; :: thesis: S2[e,f]
thus S2[e,f] by A21; :: thesis: verum
end;
end;
end;
consider F2 being Function such that
A22: ( dom F2 = X1 ^omega & ( for e being object st e in X1 ^omega holds
S2[e,F2 . e] ) ) from CLASSES1:sch 1(A6);
 A23: for n being Nat
for fs being XFinSequence of X1 st n >= 2 & dom fs = n & ( for m being non zero Nat 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 Nat st p >= 1 & p <= n - 1 holds
ex m1, m2 being non zero Nat 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 Nat; :: thesis: for fs being XFinSequence of X1 st n >= 2 & dom fs = n & ( for m being non zero Nat 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 Nat st p >= 1 & p <= n - 1 holds
ex m1, m2 being non zero Nat 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 X1; :: thesis: ( n >= 2 & dom fs = n & ( for m being non zero Nat 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 Nat st p >= 1 & p <= n - 1 holds
ex m1, m2 being non zero Nat 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 A24: n >= 2 ; :: thesis: ( not dom fs = n or ex m being non zero Nat 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 Nat st
( p >= 1 & p <= n - 1 & ( for m1, m2 being non zero Nat
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 Nat 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 Nat st
( p >= 1 & p <= n - 1 & ( for m1, m2 being non zero Nat
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 Nat 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 Nat st
( p >= 1 & p <= n - 1 & ( for m1, m2 being non zero Nat
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 Nat st p >= 1 & p <= n - 1 holds
ex m1, m2 being non zero Nat 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
A25: len fs1 = n - 1 and
A26: for p being Nat st p >= 1 & p <= n - 1 holds
ex m1, m2 being non zero Nat 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
A27: F2 . fs = Union fs1 ;
A28: for x being object st x in F2 . fs holds
ex y, z being object st x = [y,z]
proof
let x be object ; :: thesis: ( x in F2 . fs implies ex y, z being object st x = [y,z] )
assume x in F2 . fs ; :: thesis: ex y, z being object st x = [y,z]
then x in union (rng fs1) by A27, CARD_3:def 4;
then consider Y being set such that
A29: ( x in Y & Y in rng fs1 ) by TARSKI:def 4;
consider p being object such that
A30: ( p in dom fs1 & Y = fs1 . p ) by A29, FUNCT_1:def 3;
reconsider p = 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 being non zero Nat, f1 being Function of (free_magma (X,m1)),M, f2 being 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 being object such that
A32: x = [y,z] by A29, A30, A31, RELAT_1:def 1;
take y ; :: thesis: ex z being object st x = [y,z]
take z ; :: thesis: x = [y,z]
thus x = [y,z] by A32; :: thesis: verum
end;
for x, y1, y2 being object st [x,y1] in F2 . fs & [x,y2] in F2 . fs holds
y1 = y2
proof
let x, y1, y2 be object ; :: 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 A27, CARD_3:def 4;
then consider Y1 being set such that
A33: ( [x,y1] in Y1 & Y1 in rng fs1 ) by TARSKI:def 4;
consider p1 being object such that
A34: ( p1 in dom fs1 & Y1 = fs1 . p1 ) by A33, FUNCT_1:def 3;
reconsider p1 = 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 being non zero Nat, f19 being Function of (free_magma (X,m19)),M, f29 being 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 ; :: thesis: y1 = y2
then [x,y2] in union (rng fs1) by A27, CARD_3:def 4;
then consider Y2 being set such that
A38: ( [x,y2] in Y2 & Y2 in rng fs1 ) by TARSKI:def 4;
consider p2 being object such that
A39: ( p2 in dom fs1 & Y2 = fs1 . p2 ) by A38, FUNCT_1:def 3;
reconsider p2 = 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 being non zero Nat, f199 being Function of (free_magma (X,m199)),M, f299 being 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 ; :: thesis: verum
end;
then reconsider f9 = F2 . fs as Function by A28, FUNCT_1:def 1, RELAT_1:def 1;
for x being object holds
( x in free_magma (X,n) iff ex y being object st [x,y] in f9 )
proof
let x be object ; :: thesis: ( x in free_magma (X,n) iff ex y being object st [x,y] in f9 )
hereby :: thesis: ( ex y being object st [x,y] in f9 implies x in free_magma (X,n) )
assume x in free_magma (X,n) ; :: thesis: ex y being object st [x,y] in f9
then consider p, m being 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 being non zero Nat, f1 being Function of (free_magma (X,m1)),M, f2 being 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 = y; :: thesis: [x,y] in f9
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; :: thesis: verum
end;
given y being object such that A50: [x,y] in f9 ; :: thesis: x in free_magma (X,n)
[x,y] in union (rng fs1) by A27, A50, CARD_3:def 4;
then consider Y being set such that
A51: ( [x,y] in Y & Y in rng fs1 ) by TARSKI:def 4;
consider p being 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 = p as Nat by A52;
( p >= 1 & p <= n - 1 ) by A53, A25, FINSEQ_1:1;
then consider m1, m2 being non zero Nat, f1 being Function of (free_magma (X,m1)),M, f2 being 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; :: thesis: verum
end;
then A59: dom f9 = free_magma (X,n) by XTUPLE_0:def 12;
for y being object st y in rng f9 holds
y in the carrier of M
proof
let y be object ; :: 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 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 being set such that
A61: ( [x,y] in Y & Y in rng fs1 ) by TARSKI:def 4;
consider p being 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 = p as Nat by A62;
( p >= 1 & p <= n - 1 ) by A63, A25, FINSEQ_1:1;
then consider m1, m2 being non zero Nat, f1 being Function of (free_magma (X,m1)),M, f2 being 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 ; :: thesis: verum
end;
then rng f9 c= the carrier of M ;
hence F2 . fs in Funcs ((free_magma (X,n)), the carrier of M) by A59, FUNCT_2:def 2; :: thesis: verum
end;
for e being object st e in X1 ^omega holds
F2 . e in X1
proof
let e be object ; :: thesis: ( e in X1 ^omega implies F2 . e in X1 )
assume A65: e in X1 ^omega ; :: thesis: F2 . e in X1
then reconsider fs = e as XFinSequence of X1 by AFINSQ_1:def 7;
per cases ( for m being non zero Nat st m in dom fs holds
fs . m is Function of (free_magma (X,m)),M or ex m being non zero Nat st
( m in dom fs & fs . m is not Function of (free_magma (X,m)),M ) ) ;
suppose A66: for m being non zero Nat st m in dom fs holds
fs . m is Function of (free_magma (X,m)),M ; :: thesis: F2 . e in X1
then A67: ( ( dom fs = 0 implies F2 . e = {} ) & ( dom fs = 1 implies F2 . e = f ) & ( for n being Nat st n >= 2 & dom fs = n holds
ex fs1 being FinSequence st
( len fs1 = n - 1 & ( for p being Nat st p >= 1 & p <= n - 1 holds
ex m1, m2 being non zero Nat 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 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 ( dom fs = 0 or dom fs = 1 or dom fs >= 2 ) by A68, NAT_1:13;
suppose A69: dom fs = 0 ; :: thesis: F2 . e in X1
Funcs ({}, the carrier of M) = {{}} by FUNCT_5:57;
then A70: {} 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 A70, TARSKI:def 4;
hence F2 . e in X1 by A69, A67, CARD_3:def 4; :: thesis: verum
end;
suppose dom fs = 1 ; :: thesis: F2 . e in X1
hence F2 . e in X1 by A5, A66, A65, A22; :: thesis: verum
end;
suppose A71: 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 Nat st p >= 1 & p <= (dom fs) - 1 holds
ex m1, m2 being non zero Nat 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 A66, A71, A65, A22;
then A72: F2 . e in Funcs ((free_magma (X,(dom fs))), the carrier of M) by A23, A71, A66;
A73: 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 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; :: thesis: verum
end;
end;
end;
suppose ex m being non zero Nat 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, A65, A22; :: thesis: verum
end;
end;
end;
then reconsider F2 = F2 as Function of (X1 ^omega),X1 by A22, FUNCT_2:3;
deffunc H1( XFinSequence of X1) -> Element of X1 = F2 . $1;
consider F3 being sequence of X1 such that
A74: for n being Nat holds F3 . n = H1(F3 | n) from ALGSTR_4:sch 4();
 A75: for n being Nat st n > 0 holds
F3 . n is Function of (free_magma (X,n)),M
proof
defpred S3[ Nat] means for n being Nat st $1 = n & n > 0 holds
F3 . n is Function of (free_magma (X,n)),M;
A76: 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 A77: for n being Nat st n < k holds
S3[n] ; :: thesis: S3[k]
thus S3[k] :: thesis: verum
proof
let n be Nat; :: thesis: ( k = n & n > 0 implies F3 . n is Function of (free_magma (X,n)),M )
assume A78: 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
A79: for m being 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; :: thesis: ( m in dom (F3 | n) implies (F3 | n) . m is Function of (free_magma (X,m)),M )
assume A80: m in dom (F3 | n) ; :: thesis: (F3 | n) . m is Function of (free_magma (X,m)),M
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; :: thesis: verum
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 being Nat st n >= 2 & dom fs = n holds
ex fs1 being FinSequence st
( len fs1 = n - 1 & ( for p being Nat st p >= 1 & p <= n - 1 holds
ex m1, m2 being non zero Nat 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 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 ( n = 0 or n = 1 or n >= 2 ) by A87, NAT_1:13;
suppose A88: 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 A88, A83, TARSKI:def 1;
then F2 . fs in Funcs ((free_magma (X,n)), the carrier of M) by A88, 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 A89: 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 A79, A82, A22, A89, A86; :: thesis: verum
end;
suppose A90: 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 Nat st p >= 1 & p <= n - 1 holds
ex m1, m2 being non zero Nat 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 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 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 A74; :: thesis: verum
end;
end;
for k being Nat holds S3[k] from NAT_1:sch 4(A76);
 hence for n being Nat 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[ object , object ] 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);
A91: for x being object st x in X9 holds
ex y being object st
( y in the carrier of M & S3[x,y] )
proof
let x be object ; :: thesis: ( x in X9 implies ex y being object st
( y in the carrier of M & S3[x,y] ) )
assume x in X9 ; :: thesis: ex y being object 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 A75;
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
A92: for x being object st x in X9 holds
S3[x,h . x] from FUNCT_2:sch 1(A91);
 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 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 being 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; :: 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 A97: 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 A75;
hence (F3 | ((length a) + (length b))) . m is Function of (free_magma (X,m)),M by A97, FUNCT_1:47; :: thesis: verum
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: (length a) + (length b) in NAT by ORDINAL1:def 12;
dom F3 = NAT by FUNCT_2:def 1;
then A100: (length a) + (length b) c= dom F3 by A99, ORDINAL1:def 2;
dom (F3 | ((length a) + (length b))) = (dom F3) /\ ((length a) + (length b)) by RELAT_1:61
.= (length a) + (length b) by A100, XBOOLE_1:28 ;
then consider fs1 being FinSequence such that
A101: len fs1 = ((length a) + (length b)) - 1 and
A102: for p being Nat st p >= 1 & p <= ((length a) + (length b)) - 1 holds
ex m1, m2 being non zero Nat 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
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 being set such that
A104: ( [((a * b) `1),(fab . ((a * b) `1))] in Y & Y in rng fs1 ) by TARSKI:def 4;
consider p being 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 = p as Nat by A105;
( p >= 1 & p <= ((length a) + (length b)) - 1 ) by A106, A101, FINSEQ_1:1;
then consider m1, m2 being non zero Nat, f1 being Function of (free_magma (X,m1)),M, f2 being Function of (free_magma (X,m2)),M such that
A107: ( 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 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 ((length a) + (length b)) 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 ((length a) + (length b)) 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; :: 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 object st x in dom (f * ((canon_image (X,1)) ")) holds
x in dom h
proof
let x be object ; :: thesis: ( x in dom (f * ((canon_image (X,1)) ")) implies x in dom h )
assume A120: 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 A120;
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 A121: dom (f * ((canon_image (X,1)) ")) c= dom h ;
for x being object st x in (dom h) /\ (dom (f * ((canon_image (X,1)) "))) holds
h . x = (f * ((canon_image (X,1)) ")) . x
proof
let x be object ; :: 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 A122: x in dom (f * ((canon_image (X,1)) ")) by A121, XBOOLE_1:28;
A123: 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 A122;
then x in rng (canon_image (X,1)) by FUNCT_1:33;
then consider x9 being object such that
A124: ( x9 in dom (canon_image (X,1)) & x = (canon_image (X,1)) . 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: ((canon_image (X,1)) ") . x = x9 by A124, FUNCT_1:34;
set f9 = F3 . (w `2);
reconsider f9 = F3 . (w `2) as Function of (free_magma (X,(w `2))),M by A75;
A130: f9 = F3 . 1 by A128
.= H1(F3 | 1) by A74 ;
A131: for m being 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; :: 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 A75; :: thesis: verum
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 . (((canon_image (X,1)) ") . x) by A129, A130, A134, A131, A132, A22
.= (f * ((canon_image (X,1)) ")) . x by A123, A122, 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 A121; :: thesis: verum