let S be non empty non void ManySortedSign ; :: thesis:
let X be non-empty ManySortedSet of the carrier of S; :: thesis:
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:
let F be ManySortedFunction of FreeGen X, the Sorts of U1; :: thesis:
set SA = the Sorts of (FreeMSA X);
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 H₁( Symbol of (DTConMSA X)) -> Element of Union the Sorts of U1 = pi (F, the Sorts of U1,$1);
deffunc H₂( Symbol of (DTConMSA X), FinSequence, FinSequence) -> Element of Union the Sorts of U1 = pi ((@ (X,$1)),U1,$3);
consider G being Function of (TS (DTConMSA X)),(Union the Sorts of U1) such that
A1: for t being Symbol of (DTConMSA X) st t in Terminals (DTConMSA X) holds
G . (root-tree t) = H₁(t) and
A2: for nt being Symbol of (DTConMSA X)
for ts being FinSequence of TS (DTConMSA X) st nt ==> roots ts holds
G . (nt -tree ts) = H₂(nt, roots ts,G * ts) from DTCONSTR:sch 8();
deffunc H₃( object ) -> Element of bool [:(TS (DTConMSA X)),(Union the Sorts of U1):] = G | ( the Sorts of (FreeMSA X) . $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 = H₃(s) ) ) from FUNCT_1:sch 3();
reconsider h = h as ManySortedSet of the carrier of S by A3, PARTFUN1:def 2, RELAT_1:def 18;
for s being object st s in dom h holds
h . s is Function

proof

let s be object ; :: thesis:
assume s in dom h ; :: thesis:
then h . s = G | ( the Sorts of (FreeMSA X) . s) by A3;
hence h . s is Function ; :: thesis:

end;

then reconsider h = h as ManySortedFunction of the carrier of S by FUNCOP_1:def 6;
defpred S₁[ set ] means for s being SortSymbol of S st $1 in the Sorts of (FreeMSA X) . s holds
(h . s) . $1 in the Sorts of U1 . s;
A4: for nt being Symbol of (DTConMSA X)
for ts being FinSequence of TS (DTConMSA X) st nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA X) st t in rng ts holds
S₁[t] ) holds
S₁[nt -tree ts]

proof

let nt be Symbol of (DTConMSA X); :: thesis:
let ts be FinSequence of TS (DTConMSA X); :: thesis:
assume that
A5: nt ==> roots ts and
A6: for t being DecoratedTree of the carrier of (DTConMSA X) st t in rng ts holds
S₁[t] ; :: thesis:
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 (coprod X));
set rt = roots ts;
A7: [(@ (X,nt)), the carrier of S] = nt by A5, Def20;
then A8: [[(@ (X,nt)), the carrier of S],(roots ts)] in the Rules of (DTConMSA X) by A5, LANG1:def 1;
A9: [(@ (X,nt)), the carrier of S] = Sym ((@ (X,nt)),X) ;
then A10: (DenOp ((@ (X,nt)),X)) . ts = nt -tree ts by A5, A7, Def12;
dom (DenOp ((@ (X,nt)),X)) = (((FreeSort 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= ((FreeSort X) * the ResultSort of S) . (@ (X,nt)) & nt -tree ts in rng (DenOp ((@ (X,nt)),X)) ) by A10, FUNCT_1:def 3, RELAT_1:def 19;
then A11: nt -tree ts in ( the Sorts of (FreeMSA X) * 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 (coprod X))) * by A8, ZFMISC_1:87;
A14: len rt = len (the_arity_of (@ (X,nt))) by A8, Th5;
A15: dom rt = Seg (len rt) by FINSEQ_1:def 3;
dom the Sorts of (FreeMSA X) = the carrier of S by PARTFUN1:def 2;
then A16: dom ( the Sorts of (FreeMSA X) * (the_arity_of (@ (X,nt)))) = dom (the_arity_of (@ (X,nt))) by A13, RELAT_1:27;
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 A13, RELAT_1:27;
A19: ( dom rt = dom ts & Seg (len (the_arity_of (@ (X,nt)))) = dom (the_arity_of (@ (X,nt))) ) by FINSEQ_1:def 3, TREES_3:def 18;
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

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 A12, RELAT_1:27;
let s be SortSymbol of S; :: thesis:
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 (FreeMSA X) = the carrier of S by PARTFUN1:def 2;
then dom ( the Sorts of (FreeMSA X) * the ResultSort of S) = dom the ResultSort of S by A12, RELAT_1:27;
then nt -tree ts in the Sorts of (FreeMSA X) . ( the ResultSort of S . (@ (X,nt))) by A32, A11, FUNCT_1:12;
then A33: nt -tree ts in the Sorts of (FreeMSA X) . (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 A17, Th1 ;
then A34: G * ts in Args ((@ (X,nt)),U1) by A20, A18, A14, A15, A19, A22, CARD_3:9;
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 A34, A31, FUNCT_1:def 3, RELAT_1:def 19;
then A35: pi ((@ (X,nt)),U1,(G * ts)) in Result ((@ (X,nt)),U1) ;
assume A36: nt -tree ts in the Sorts of (FreeMSA X) . s ; :: thesis:
A37: the_result_sort_of (@ (X,nt)) = s by A33, A36, XBOOLE_0:3, Th12;
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 (FreeMSA X) . (the_result_sort_of (@ (X,nt))))) . (nt -tree ts) by A33, FUNCT_1:49;
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 A30, A32, FUNCT_1:12
.= 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:

end;

A39: for t being Symbol of (DTConMSA X) st t in Terminals (DTConMSA X) holds
S₁[ root-tree t]

proof

let t be Symbol of (DTConMSA X); :: thesis:
assume A40: t in Terminals (DTConMSA X) ; :: thesis:
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 = { (root-tree tt) where tt is Symbol of (DTConMSA X) : ( tt in Terminals (DTConMSA X) & tt `2 = s ) } ;
set a = root-tree t;
A42: t `2 = s by A41;
then A43: root-tree t in { (root-tree tt) where tt is Symbol of (DTConMSA X) : ( tt in Terminals (DTConMSA X) & tt `2 = s ) } by A40;
let s1 be SortSymbol of S; :: thesis:
reconsider f = F . s as Function of ((FreeGen X) . s),( the Sorts of U1 . s) ;
A44: dom f = (FreeGen X) . s by FUNCT_2:def 1;
A45: { (root-tree tt) where tt is Symbol of (DTConMSA X) : ( tt in Terminals (DTConMSA X) & tt `2 = s ) } = FreeGen (s,X) by Th13;
then (FreeGen X) . s = { (root-tree tt) where tt is Symbol of (DTConMSA X) : ( tt in Terminals (DTConMSA X) & tt `2 = s ) } by Def16;
then A46: ( rng f c= the Sorts of U1 . s & f . (root-tree t) in rng f ) by A43, A44, FUNCT_1:def 3, RELAT_1:def 19;
assume A47: root-tree t in the Sorts of (FreeMSA X) . s1 ; :: thesis:

A48: now :: thesis:

root-tree t in ((FreeSort X) . s) /\ ((FreeSort X) . s1) by A43, A45, A47, XBOOLE_0:def 4;
then A49: (FreeSort X) . s meets (FreeSort X) . s1 ;
assume s <> s1 ; :: thesis:
hence contradiction by A49, Th12; :: thesis:

end;

h . s = G | ( the Sorts of (FreeMSA X) . s) by A3;
then (h . s) . (root-tree t) = G . (root-tree t) by A43, A45, FUNCT_1:49
.= pi (F, the Sorts of U1,t) by A1, A40
.= f . (root-tree t) by A40, A42, Def19 ;
hence (h . s1) . (root-tree t) in the Sorts of U1 . s1 by A46, A48; :: thesis:

end;

A50: for t being DecoratedTree of the carrier of (DTConMSA X) st t in TS (DTConMSA X) holds
S₁[t] from DTCONSTR:sch 7(A39, A4);
for s being object st s in the carrier of S holds
h . s is Function of ( the Sorts of (FreeMSA X) . s),( the Sorts of U1 . s)

proof

let x be object ; :: thesis:
assume x in the carrier of S ; :: thesis:
then reconsider s = x as SortSymbol of S ;
A51: dom G = TS (DTConMSA X) by FUNCT_2:def 1
.= union (rng the Sorts of (FreeMSA X)) by Th11 ;
dom the Sorts of (FreeMSA X) = the carrier of S by PARTFUN1:def 2;
then A52: the Sorts of (FreeMSA X) . s in rng the Sorts of (FreeMSA X) by FUNCT_1:def 3;
A53: h . s = G | ( the Sorts of (FreeMSA X) . s) by A3;
then A54: dom (h . s) = the Sorts of (FreeMSA X) . s by A51, A52, RELAT_1:62, ZFMISC_1:74;
A55: the Sorts of (FreeMSA X) . s c= dom G by A51, A52, ZFMISC_1:74;
rng (h . s) c= the Sorts of U1 . s

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in rng (h . s) ; :: thesis:
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 (DTConMSA X) by A55, A54, A56, FUNCT_2:def 1;
T in the Sorts of (FreeMSA X) . s by A53, A51, A52, A56, RELAT_1:62, ZFMISC_1:74;
hence a in the Sorts of U1 . s by A50, A57; :: thesis:

end;

hence h . x is Function of ( the Sorts of (FreeMSA X) . x),( the Sorts of U1 . x) by A54, FUNCT_2:def 1, RELSET_1:4; :: thesis:

end;

then reconsider h = h as ManySortedFunction of (FreeMSA X),U1 by PBOOLE:def 15;
take h ; :: thesis:
thus h is_homomorphism FreeMSA X,U1 :: thesis:

proof

( rng the ResultSort of S c= the carrier of S & dom the Sorts of (FreeMSA X) = the carrier of S ) by PARTFUN1:def 2, RELAT_1:def 19;
then A58: ( dom the ResultSort of S = the carrier' of S & dom ( the Sorts of (FreeMSA X) * the ResultSort of S) = dom the ResultSort of S ) by FUNCT_2:def 1, RELAT_1:27;
let o be OperSymbol of S; :: according to MSUALG_3:def 7 :: thesis:
assume Args (o,(FreeMSA X)) <> {} ; :: thesis:
let x be Element of Args (o,(FreeMSA X)); :: thesis:
set rs = the_result_sort_of o;
set DA = Den (o,(FreeMSA X));
set D1 = Den (o,U1);
set OU = [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X));
set ar = the_arity_of o;
A59: the_arity_of o = the Arity of S . o by MSUALG_1:def 1;
A60: Args (o,(FreeMSA X)) = (((FreeSort X) #) * the Arity of S) . o by MSUALG_1:def 4;
then reconsider p = x as FinSequence of TS (DTConMSA X) by Th8;
A61: Sym (o,X) ==> roots p by A60, Th10;
then A62: @ (X,(Sym (o,X))) = o by Def20;
A63: dom (G * p) = dom p by FINSEQ_3:120;
A64: x in (((FreeSort X) #) * 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 (the_arity_of o) c= the carrier of S & dom the Sorts of (FreeMSA X) = the carrier of S ) by FINSEQ_1:def 4, PARTFUN1:def 2;
then A66: dom ( the Sorts of (FreeMSA X) * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27;
set rt = roots p;
let a be object ; :: thesis:
assume A67: a in dom p ; :: thesis:
then reconsider n = a as Nat ;
A68: [[o, the carrier of S],(roots p)] in the Rules of (DTConMSA X) by A61, LANG1:def 1;
then reconsider rt = roots p as Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by ZFMISC_1:87;
A69: len rt = len (the_arity_of o) by A68, Th5;
A70: ( (G * p) . n = G . (x . n) & (h # x) . n = (h . ((the_arity_of o) /. n)) . (x . n) ) by A63, A67, FINSEQ_3:120, MSUALG_3:def 6;
A71: h . ((the_arity_of o) /. n) = G | ( the Sorts of (FreeMSA X) . ((the_arity_of o) /. n)) by A3;
A72: Seg (len rt) = dom rt by FINSEQ_1:def 3;
A73: ( dom rt = dom p & Seg (len (the_arity_of o)) = dom (the_arity_of o) ) by FINSEQ_1:def 3, TREES_3:def 18;
p in product ((FreeSort X) * (the_arity_of o)) by A64, A59, Th1;
then A74: p . n in ((FreeSort X) * (the_arity_of o)) . n by A67, A66, A69, A72, A73, CARD_3:9;
((FreeSort X) * (the_arity_of o)) . n = the Sorts of (FreeMSA X) . ((the_arity_of o) . n) by A67, A66, A69, A72, A73, FUNCT_1:12
.= the Sorts of (FreeMSA X) . ((the_arity_of o) /. n) by A67, A69, A72, A73, PARTFUN1:def 6 ;
hence (G * p) . a = (h # x) . a by A70, A71, A74, FUNCT_1:49; :: thesis:

end;

end;

for x being object st x in the carrier of S holds
(h || (FreeGen X)) . x = F . x

proof

set hf = h || (FreeGen X);
let x be object ; :: thesis:
assume x in the carrier of S ; :: thesis:
then reconsider s = x as SortSymbol of S ;
A81: dom (h . s) = the Sorts of (FreeMSA X) . s by FUNCT_2:def 1;
A82: dom ((h || (FreeGen X)) . s) = (FreeGen X) . s by FUNCT_2:def 1;
A83: (FreeGen X) . s = FreeGen (s,X) by Def16;
A84: (h || (FreeGen X)) . s = (h . s) | ((FreeGen X) . s) by Def1;
A85: for a being object st a in (FreeGen X) . s holds
((h || (FreeGen X)) . s) . a = (F . s) . a

proof

let a be object ; :: thesis:
A86: h . s = G | ( the Sorts of (FreeMSA X) . s) by A3;
assume A87: a in (FreeGen X) . s ; :: thesis:
then a in { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) } by A83, Th13;
then consider t being Symbol of (DTConMSA X) such that
A88: ( a = root-tree t & t in Terminals (DTConMSA X) ) and
A89: t `2 = s ;
thus ((h || (FreeGen X)) . s) . a = (h . s) . a by A84, A82, A87, FUNCT_1:47
.= G . a by A81, A83, A87, A86, FUNCT_1:47
.= pi (F, the Sorts of U1,t) by A1, A88
.= (F . s) . a by A88, A89, Def19 ; :: thesis:

end;

dom (F . s) = (FreeGen X) . s by FUNCT_2:def 1;
hence (h || (FreeGen X)) . x = F . x by A82, A85, FUNCT_1:2; :: thesis:

end;

hence h || (FreeGen X) = F ; :: thesis: