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