let S be non empty non void ManySortedSign ; :: thesis: for X being V5() ManySortedSet of the carrier of S holds FreeGen X is free
let X be V5() ManySortedSet of the carrier of S; :: thesis: FreeGen X is free
set D = DTConMSA X;
set FA = FreeMSA X;
set FG = FreeGen X;
let U1 be non-empty MSAlgebra over S; :: according to MSAFREE:def 5 :: thesis: for f being ManySortedFunction of FreeGen X, the Sorts of U1 ex h being ManySortedFunction of (),U1 st
( h is_homomorphism FreeMSA X,U1 & h || () = f )

let F be ManySortedFunction of FreeGen X, the Sorts of U1; :: thesis: ex h being ManySortedFunction of (),U1 st
( h is_homomorphism FreeMSA X,U1 & h || () = F )

set SA = the Sorts of ();
set AR = the Arity of S;
set S1 = the Sorts of U1;
set O = the carrier' of S;
set RS = the ResultSort of S;
set DU = Union the Sorts of U1;
deffunc H1( Symbol of ()) -> Element of Union the Sorts of U1 = pi (F, the Sorts of U1,\$1);
deffunc H2( Symbol of (), FinSequence, FinSequence) -> Element of Union the Sorts of U1 = pi ((@ (X,\$1)),U1,\$3);
consider G being Function of (TS ()),(Union the Sorts of U1) such that
A1: for t being Symbol of () st t in Terminals () holds
G . () = H1(t) and
A2: for nt being Symbol of ()
for ts being FinSequence of TS () st nt ==> roots ts holds
G . (nt -tree ts) = H2(nt, roots ts,G * ts) from deffunc H3( object ) -> Element of bool [:(TS ()),(Union the Sorts of U1):] = G | ( the Sorts of () . \$1);
consider h being Function such that
A3: ( dom h = the carrier of S & ( for s being object st s in the carrier of S holds
h . s = H3(s) ) ) from reconsider h = h as ManySortedSet of the carrier of S by ;
for s being object st s in dom h holds
h . s is Function
proof
let s be object ; :: thesis: ( s in dom h implies h . s is Function )
assume s in dom h ; :: thesis: h . s is Function
then h . s = G | ( the Sorts of () . s) by A3;
hence h . s is Function ; :: thesis: verum
end;
then reconsider h = h as ManySortedFunction of the carrier of S by FUNCOP_1:def 6;
defpred S1[ set ] means for s being SortSymbol of S st \$1 in the Sorts of () . s holds
(h . s) . \$1 in the Sorts of U1 . s;
A4: for nt being Symbol of ()
for ts being FinSequence of TS () st nt ==> roots ts & ( for t being DecoratedTree of the carrier of () st t in rng ts holds
S1[t] ) holds
S1[nt -tree ts]
proof
let nt be Symbol of (); :: thesis: for ts being FinSequence of TS () st nt ==> roots ts & ( for t being DecoratedTree of the carrier of () st t in rng ts holds
S1[t] ) holds
S1[nt -tree ts]

let ts be FinSequence of TS (); :: thesis: ( nt ==> roots ts & ( for t being DecoratedTree of the carrier of () st t in rng ts holds
S1[t] ) implies S1[nt -tree ts] )

assume that
A5: nt ==> roots ts and
A6: for t being DecoratedTree of the carrier of () st t in rng ts holds
S1[t] ; :: thesis: S1[nt -tree ts]
set p = G * ts;
set o = @ (X,nt);
set ar = the_arity_of (@ (X,nt));
set rs = the_result_sort_of (@ (X,nt));
set OU = [: the carrier' of S,{ the carrier of S}:] \/ (Union ());
set rt = roots ts;
A7: [(@ (X,nt)), the carrier of S] = nt by ;
then A8: [[(@ (X,nt)), the carrier of S],(roots ts)] in the Rules of () by ;
A9: [(@ (X,nt)), the carrier of S] = Sym ((@ (X,nt)),X) ;
then A10: (DenOp ((@ (X,nt)),X)) . ts = nt -tree ts by ;
dom (DenOp ((@ (X,nt)),X)) = ((() #) * the Arity of S) . (@ (X,nt)) by FUNCT_2:def 1;
then ts in dom (DenOp ((@ (X,nt)),X)) by A5, A7, A9, Th10;
then ( rng (DenOp ((@ (X,nt)),X)) c= (() * the ResultSort of S) . (@ (X,nt)) & nt -tree ts in rng (DenOp ((@ (X,nt)),X)) ) by ;
then A11: nt -tree ts in ( the Sorts of () * the ResultSort of S) . (@ (X,nt)) ;
set ppi = pi ((@ (X,nt)),U1,(G * ts));
A12: rng the ResultSort of S c= the carrier of S by RELAT_1:def 19;
A13: rng (the_arity_of (@ (X,nt))) c= the carrier of S by FINSEQ_1:def 4;
reconsider rt = roots ts as Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union ())) * by ;
A14: len rt = len (the_arity_of (@ (X,nt))) by ;
A15: dom rt = Seg (len rt) by FINSEQ_1:def 3;
dom the Sorts of () = the carrier of S by PARTFUN1:def 2;
then A16: dom ( the Sorts of () * (the_arity_of (@ (X,nt)))) = dom (the_arity_of (@ (X,nt))) by ;
A17: the_arity_of (@ (X,nt)) = the Arity of S . (@ (X,nt)) by MSUALG_1:def 1;
dom the Sorts of U1 = the carrier of S by PARTFUN1:def 2;
then A18: dom ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) = dom (the_arity_of (@ (X,nt))) by ;
A19: ( dom rt = dom ts & Seg (len (the_arity_of (@ (X,nt)))) = dom (the_arity_of (@ (X,nt))) ) by ;
A20: dom (G * ts) = dom ts by FINSEQ_3:120;
then A21: dom (G * ts) = dom ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) by A18, A8, A15, A19, Th5;
A22: for x being object st x in dom ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) holds
(G * ts) . x in ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) . x
proof
let x be object ; :: thesis: ( x in dom ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) implies (G * ts) . x in ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) . x )
assume A23: x in dom ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) ; :: thesis: (G * ts) . x in ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) . x
then reconsider n = x as Nat ;
A24: ts . n in rng ts by ;
rng ts c= TS () by FINSEQ_1:def 4;
then reconsider t = ts . n as Element of TS () by A24;
A25: (G * ts) . n = G . (ts . n) by ;
(the_arity_of (@ (X,nt))) . x in rng (the_arity_of (@ (X,nt))) by ;
then reconsider s = (the_arity_of (@ (X,nt))) . x as SortSymbol of S by A13;
A26: h . s = G | ( the Sorts of () . s) by A3;
dom the Sorts of () = the carrier of S by PARTFUN1:def 2;
then A27: the Sorts of () . s in rng the Sorts of () by FUNCT_1:def 3;
dom G = TS () by FUNCT_2:def 1
.= union (rng the Sorts of ()) by Th11 ;
then A28: dom (h . s) = the Sorts of () . s by ;
ts in ((() #) * the Arity of S) . (@ (X,nt)) by A5, A7, A9, Th10;
then ts in product (() * (the_arity_of (@ (X,nt)))) by ;
then ts . x in (() * (the_arity_of (@ (X,nt)))) . x by ;
then A29: ts . x in () . ((the_arity_of (@ (X,nt))) . x) by ;
then (h . s) . t in the Sorts of U1 . s by ;
then G . t in the Sorts of U1 . s by ;
hence (G * ts) . x in ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) . x by ; :: thesis: verum
end;
dom the Sorts of U1 = the carrier of S by PARTFUN1:def 2;
then A30: dom ( the Sorts of U1 * the ResultSort of S) = dom the ResultSort of S by ;
let s be SortSymbol of S; :: thesis: ( nt -tree ts in the Sorts of () . s implies (h . s) . (nt -tree ts) in the Sorts of U1 . s )
A31: dom (Den ((@ (X,nt)),U1)) = Args ((@ (X,nt)),U1) by FUNCT_2:def 1;
A32: dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1;
dom the Sorts of () = the carrier of S by PARTFUN1:def 2;
then dom ( the Sorts of () * the ResultSort of S) = dom the ResultSort of S by ;
then nt -tree ts in the Sorts of () . ( the ResultSort of S . (@ (X,nt))) by ;
then A33: nt -tree ts in the Sorts of () . (the_result_sort_of (@ (X,nt))) by MSUALG_1:def 2;
Args ((@ (X,nt)),U1) = (( the Sorts of U1 #) * the Arity of S) . (@ (X,nt)) by MSUALG_1:def 4
.= product ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) by ;
then A34: G * ts in Args ((@ (X,nt)),U1) by ;
then pi ((@ (X,nt)),U1,(G * ts)) = (Den ((@ (X,nt)),U1)) . (G * ts) by Def21;
then ( rng (Den ((@ (X,nt)),U1)) c= Result ((@ (X,nt)),U1) & pi ((@ (X,nt)),U1,(G * ts)) in rng (Den ((@ (X,nt)),U1)) ) by ;
then A35: pi ((@ (X,nt)),U1,(G * ts)) in Result ((@ (X,nt)),U1) ;
assume A36: nt -tree ts in the Sorts of () . s ; :: thesis: (h . s) . (nt -tree ts) in the Sorts of U1 . s
A37: the_result_sort_of (@ (X,nt)) = s by ;
G . (nt -tree ts) = pi ((@ (X,nt)),U1,(G * ts)) by A2, A5;
then A38: pi ((@ (X,nt)),U1,(G * ts)) = (G | ( the Sorts of () . (the_result_sort_of (@ (X,nt))))) . (nt -tree ts) by ;
Result ((@ (X,nt)),U1) = ( the Sorts of U1 * the ResultSort of S) . (@ (X,nt)) by MSUALG_1:def 5
.= the Sorts of U1 . ( the ResultSort of S . (@ (X,nt))) by
.= the Sorts of U1 . (the_result_sort_of (@ (X,nt))) by MSUALG_1:def 2 ;
hence (h . s) . (nt -tree ts) in the Sorts of U1 . s by A3, A35, A38, A37; :: thesis: verum
end;
A39: for t being Symbol of () st t in Terminals () holds
S1[ root-tree t]
proof
let t be Symbol of (); :: thesis: ( t in Terminals () implies S1[ root-tree t] )
assume A40: t in Terminals () ; :: thesis: S1[ root-tree t]
then consider s being SortSymbol of S, x being set such that
x in X . s and
A41: t = [x,s] by Th7;
set E = { () where tt is Symbol of () : ( tt in Terminals () & tt `2 = s ) } ;
set a = root-tree t;
A42: t `2 = s by A41;
then A43: root-tree t in { () where tt is Symbol of () : ( tt in Terminals () & tt `2 = s ) } by A40;
let s1 be SortSymbol of S; :: thesis: ( root-tree t in the Sorts of () . s1 implies (h . s1) . () in the Sorts of U1 . s1 )
reconsider f = F . s as Function of (() . s),( the Sorts of U1 . s) ;
A44: dom f = () . s by FUNCT_2:def 1;
A45: { (root-tree tt) where tt is Symbol of () : ( tt in Terminals () & tt `2 = s ) } = FreeGen (s,X) by Th13;
then (FreeGen X) . s = { () where tt is Symbol of () : ( tt in Terminals () & tt `2 = s ) } by Def16;
then A46: ( rng f c= the Sorts of U1 . s & f . () in rng f ) by ;
assume A47: root-tree t in the Sorts of () . s1 ; :: thesis: (h . s1) . () in the Sorts of U1 . s1
A48: now :: thesis: not s <> s1
root-tree t in (() . s) /\ (() . s1) by ;
then A49: (FreeSort X) . s meets () . s1 ;
assume s <> s1 ; :: thesis: contradiction
hence contradiction by A49, Th12; :: thesis: verum
end;
h . s = G | ( the Sorts of () . s) by A3;
then (h . s) . () = G . () by
.= pi (F, the Sorts of U1,t) by
.= f . () by ;
hence (h . s1) . () in the Sorts of U1 . s1 by ; :: thesis: verum
end;
A50: for t being DecoratedTree of the carrier of () st t in TS () holds
S1[t] from for s being object st s in the carrier of S holds
h . s is Function of ( the Sorts of () . s),( the Sorts of U1 . s)
proof
let x be object ; :: thesis: ( x in the carrier of S implies h . x is Function of ( the Sorts of () . x),( the Sorts of U1 . x) )
assume x in the carrier of S ; :: thesis: h . x is Function of ( the Sorts of () . x),( the Sorts of U1 . x)
then reconsider s = x as SortSymbol of S ;
A51: dom G = TS () by FUNCT_2:def 1
.= union (rng the Sorts of ()) by Th11 ;
dom the Sorts of () = the carrier of S by PARTFUN1:def 2;
then A52: the Sorts of () . s in rng the Sorts of () by FUNCT_1:def 3;
A53: h . s = G | ( the Sorts of () . s) by A3;
then A54: dom (h . s) = the Sorts of () . s by ;
A55: the Sorts of () . s c= dom G by ;
rng (h . s) c= the Sorts of U1 . s
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng (h . s) or a in the Sorts of U1 . s )
assume a in rng (h . s) ; :: thesis: a in the Sorts of U1 . s
then consider T being object such that
A56: T in dom (h . s) and
A57: (h . s) . T = a by FUNCT_1:def 3;
reconsider T = T as Element of TS () by ;
T in the Sorts of () . s by ;
hence a in the Sorts of U1 . s by ; :: thesis: verum
end;
hence h . x is Function of ( the Sorts of () . x),( the Sorts of U1 . x) by ; :: thesis: verum
end;
then reconsider h = h as ManySortedFunction of (),U1 by PBOOLE:def 15;
take h ; :: thesis: ( h is_homomorphism FreeMSA X,U1 & h || () = F )
thus h is_homomorphism FreeMSA X,U1 :: thesis: h || () = F
proof
( rng the ResultSort of S c= the carrier of S & dom the Sorts of () = the carrier of S ) by ;
then A58: ( dom the ResultSort of S = the carrier' of S & dom ( the Sorts of () * the ResultSort of S) = dom the ResultSort of S ) by ;
let o be OperSymbol of S; :: according to MSUALG_3:def 7 :: thesis: ( Args (o,()) = {} or for b1 being Element of Args (o,()) holds (h . ) . ((Den (o,())) . b1) = (Den (o,U1)) . (h # b1) )
assume Args (o,()) <> {} ; :: thesis: for b1 being Element of Args (o,()) holds (h . ) . ((Den (o,())) . b1) = (Den (o,U1)) . (h # b1)
let x be Element of Args (o,()); :: thesis: (h . ) . ((Den (o,())) . x) = (Den (o,U1)) . (h # x)
set rs = the_result_sort_of o;
set DA = Den (o,());
set D1 = Den (o,U1);
set OU = [: the carrier' of S,{ the carrier of S}:] \/ (Union ());
set ar = the_arity_of o;
A59: the_arity_of o = the Arity of S . o by MSUALG_1:def 1;
A60: Args (o,()) = ((() #) * the Arity of S) . o by MSUALG_1:def 4;
then reconsider p = x as FinSequence of TS () by Th8;
A61: Sym (o,X) ==> roots p by ;
then A62: @ (X,(Sym (o,X))) = o by Def20;
A63: dom (G * p) = dom p by FINSEQ_3:120;
A64: x in ((() #) * the Arity of S) . o by A60;
A65: for a being object st a in dom p holds
(G * p) . a = (h # x) . a
proof
( rng () c= the carrier of S & dom the Sorts of () = the carrier of S ) by ;
then A66: dom ( the Sorts of () * ()) = dom () by RELAT_1:27;
set rt = roots p;
let a be object ; :: thesis: ( a in dom p implies (G * p) . a = (h # x) . a )
assume A67: a in dom p ; :: thesis: (G * p) . a = (h # x) . a
then reconsider n = a as Nat ;
A68: [[o, the carrier of S],()] in the Rules of () by ;
then reconsider rt = roots p as Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union ())) * by ZFMISC_1:87;
A69: len rt = len () by ;
A70: ( (G * p) . n = G . (x . n) & (h # x) . n = (h . (() /. n)) . (x . n) ) by ;
A71: h . (() /. n) = G | ( the Sorts of () . (() /. n)) by A3;
A72: Seg (len rt) = dom rt by FINSEQ_1:def 3;
A73: ( dom rt = dom p & Seg (len ()) = dom () ) by ;
p in product (() * ()) by ;
then A74: p . n in (() * ()) . n by ;
(() * ()) . n = the Sorts of () . (() . n) by
.= the Sorts of () . (() /. n) by ;
hence (G * p) . a = (h # x) . a by ; :: thesis: verum
end;
dom (h # x) = dom () by MSUALG_3:6;
then A75: G * p = h # x by ;
A76: h . = G | ( the Sorts of () . ) by A3;
A77: dom (DenOp (o,X)) = ((() #) * the Arity of S) . o by FUNCT_2:def 1;
(DenOp (o,X)) . p = (Sym (o,X)) -tree p by ;
then ( rng (DenOp (o,X)) c= (() * the ResultSort of S) . o & (Sym (o,X)) -tree p in rng (DenOp (o,X)) ) by ;
then (Sym (o,X)) -tree p in ( the Sorts of () * the ResultSort of S) . o ;
then (Sym (o,X)) -tree p in the Sorts of () . ( the ResultSort of S . o) by ;
then A78: (Sym (o,X)) -tree p in the Sorts of () . by MSUALG_1:def 2;
dom the Sorts of () = the carrier of S by PARTFUN1:def 2;
then A79: the Sorts of () . in rng the Sorts of () by FUNCT_1:def 3;
dom G = TS () by FUNCT_2:def 1
.= union (rng the Sorts of ()) by Th11 ;
then A80: dom (h . ) = the Sorts of () . by ;
Den (o,()) = () . o by MSUALG_1:def 6
.= DenOp (o,X) by Def13 ;
then (Den (o,())) . x = (Sym (o,X)) -tree p by ;
hence (h . ) . ((Den (o,())) . x) = G . ((Sym (o,X)) -tree p) by
.= pi ((@ (X,(Sym (o,X)))),U1,(G * p)) by
.= (Den (o,U1)) . (h # x) by ;
:: thesis: verum
end;
for x being object st x in the carrier of S holds
(h || ()) . x = F . x
proof
set hf = h || ();
let x be object ; :: thesis: ( x in the carrier of S implies (h || ()) . x = F . x )
assume x in the carrier of S ; :: thesis: (h || ()) . x = F . x
then reconsider s = x as SortSymbol of S ;
A81: dom (h . s) = the Sorts of () . s by FUNCT_2:def 1;
A82: dom ((h || ()) . s) = () . s by FUNCT_2:def 1;
A83: (FreeGen X) . s = FreeGen (s,X) by Def16;
A84: (h || ()) . s = (h . s) | (() . s) by Def1;
A85: for a being object st a in () . s holds
((h || ()) . s) . a = (F . s) . a
proof
let a be object ; :: thesis: ( a in () . s implies ((h || ()) . s) . a = (F . s) . a )
A86: h . s = G | ( the Sorts of () . s) by A3;
assume A87: a in () . s ; :: thesis: ((h || ()) . s) . a = (F . s) . a
then a in { () where t is Symbol of () : ( t in Terminals () & t `2 = s ) } by ;
then consider t being Symbol of () such that
A88: ( a = root-tree t & t in Terminals () ) and
A89: t `2 = s ;
thus ((h || ()) . s) . a = (h . s) . a by
.= G . a by
.= pi (F, the Sorts of U1,t) by
.= (F . s) . a by ; :: thesis: verum
end;
dom (F . s) = () . s by FUNCT_2:def 1;
hence (h || ()) . x = F . x by ; :: thesis: verum
end;
hence h || () = F ; :: thesis: verum