let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of S
for w being ManySortedFunction of X, the carrier of S --> NAT ex h being ManySortedFunction of (Free (S,X)),(TermAlg S) st
( h is_homomorphism Free (S,X), TermAlg S & ( for s being SortSymbol of S
for t being Element of (Free (S,X)),s holds # (t,w) = (h . s) . t ) )
let X be non-empty ManySortedSet of S; :: thesis: for w being ManySortedFunction of X, the carrier of S --> NAT ex h being ManySortedFunction of (Free (S,X)),(TermAlg S) st
( h is_homomorphism Free (S,X), TermAlg S & ( for s being SortSymbol of S
for t being Element of (Free (S,X)),s holds # (t,w) = (h . s) . t ) )
let w be ManySortedFunction of X, the carrier of S --> NAT; :: thesis: ex h being ManySortedFunction of (Free (S,X)),(TermAlg S) st
( h is_homomorphism Free (S,X), TermAlg S & ( for s being SortSymbol of S
for t being Element of (Free (S,X)),s holds # (t,w) = (h . s) . t ) )
A1: TermAlg S = Free (S,( the carrier of S --> NAT)) by MSAFREE3:31;
reconsider G = FreeGen X as non-empty GeneratorSet of Free (S,X) by MSAFREE3:31;
deffunc H₂( SortSymbol of S, Element of G . $1) -> set = root-tree [((w . $1) . (($2 . {}) `1)),$1];
A2: for s being SortSymbol of S
for x being Element of G . s holds H₂(s,x) in the Sorts of (TermAlg S) . s

proof

let s be SortSymbol of S; :: thesis: for x being Element of G . s holds H₂(s,x) in the Sorts of (TermAlg S) . s
let x be Element of G . s; :: thesis: H₂(s,x) in the Sorts of (TermAlg S) . s
G . s = FreeGen (s,X) by MSAFREE:def 16;
then consider y being set such that
A3: ( y in X . s & x = root-tree [y,s] ) by MSAFREE:def 15;
x . {} = [y,s] by A3, TREES_4:3;
then reconsider x1 = (x . {}) `1 as Element of X . s by A3;
A4: (w . s) . x1 in ( the carrier of S --> NAT) . s ;
then reconsider t = H₂(s,x) as Term of S,( the carrier of S --> NAT) by MSATERM:4;
t in FreeSort (( the carrier of S --> NAT),(the_sort_of t)) by MSATERM:def 5;
then t in FreeSort (( the carrier of S --> NAT),s) by A4;
hence H₂(s,x) in the Sorts of (TermAlg S) . s by MSAFREE:def 11; :: thesis: verum

end;

consider f being ManySortedFunction of G, the Sorts of (TermAlg S) such that
A5: for s being SortSymbol of S
for x being Element of G . s holds (f . s) . x = H₂(s,x) from MSAFREE4:sch 2(A2);
( FreeGen X is free & FreeMSA X = Free (S,X) ) by MSAFREE3:31;
then consider h being ManySortedFunction of (Free (S,X)),(TermAlg S) such that
A6: ( h is_homomorphism Free (S,X), TermAlg S & h || G = f ) ;
set t = the Element of (Free (S,X));
consider F being ManySortedSet of S -Terms X such that
A7: ( # ( the Element of (Free (S,X)),w) = F . the Element of (Free (S,X)) & ( for s being SortSymbol of S
for x being Element of X . s holds F . (root-tree [x,s]) = root-tree [((w . s) . x),s] ) & ( for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) holds F . ((Sym (o,X)) -tree p) = (Sym (o,( the carrier of S --> NAT))) -tree (F * p) ) ) by Def15;
take h ; :: thesis: ( h is_homomorphism Free (S,X), TermAlg S & ( for s being SortSymbol of S
for t being Element of (Free (S,X)),s holds # (t,w) = (h . s) . t ) )
thus h is_homomorphism Free (S,X), TermAlg S by A6; :: thesis: for s being SortSymbol of S
for t being Element of (Free (S,X)),s holds # (t,w) = (h . s) . t
let s be SortSymbol of S; :: thesis: for t being Element of (Free (S,X)),s holds # (t,w) = (h . s) . t
let t be Element of (Free (S,X)),s; :: thesis: # (t,w) = (h . s) . t
defpred S₁[ DecoratedTree] means for s being SortSymbol of S st $1 in the Sorts of (Free (S,X)) . s holds
# ($1,w) = (h . s) . $1;
A8: for s being SortSymbol of S
for x being Element of X . s holds S₁[ root-tree [x,s]]

proof

let s be SortSymbol of S; :: thesis: for x being Element of X . s holds S₁[ root-tree [x,s]]
let x be Element of X . s; :: thesis: S₁[ root-tree [x,s]]
reconsider t = root-tree [x,s] as Term of S,X by MSATERM:4;
let s1 be SortSymbol of S; :: thesis: ( root-tree [x,s] in the Sorts of (Free (S,X)) . s1 implies # ((root-tree [x,s]),w) = (h . s1) . (root-tree [x,s]) )
assume root-tree [x,s] in the Sorts of (Free (S,X)) . s1 ; :: thesis: # ((root-tree [x,s]),w) = (h . s1) . (root-tree [x,s])
then t in the Sorts of (FreeMSA X) . s1 by MSAFREE3:31;
then ( s = the_sort_of t & t in FreeSort (X,s1) ) by MSAFREE:def 11, MSATERM:14;
then A9: s = s1 by MSATERM:def 5;
t in FreeGen (s,X) by MSAFREE:def 15;
then reconsider q = t as Element of G . s by MSAFREE:def 16;
t is Element of (FreeMSA X) by MSATERM:13;
then t is Element of (Free (S,X)) by MSAFREE3:31;
hence # ((root-tree [x,s]),w) = F . t by A7, Th55
.= root-tree [((w . s) . x),s] by A7
.= root-tree [((w . s) . ([x,s] `1)),s]
.= H₂(s,q) by TREES_4:3
.= (f . s) . t by A5
.= ((h . s) | (G . s)) . q by A6, MSAFREE:def 1
.= (h . s1) . (root-tree [x,s]) by A9, FUNCT_1:49 ;
:: thesis: verum

end;

A10: for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) st ( for t being Term of S,X st t in rng p holds
S₁[t] ) holds
S₁[[o, the carrier of S] -tree p]

proof

let o be OperSymbol of S; :: thesis: for p being ArgumentSeq of Sym (o,X) st ( for t being Term of S,X st t in rng p holds
S₁[t] ) holds
S₁[[o, the carrier of S] -tree p]
let p be ArgumentSeq of Sym (o,X); :: thesis: ( ( for t being Term of S,X st t in rng p holds
S₁[t] ) implies S₁[[o, the carrier of S] -tree p] )
assume A11: for t being Term of S,X st t in rng p holds
S₁[t] ; :: thesis: S₁[[o, the carrier of S] -tree p]
let s be SortSymbol of S; :: thesis: ( [o, the carrier of S] -tree p in the Sorts of (Free (S,X)) . s implies # (([o, the carrier of S] -tree p),w) = (h . s) . ([o, the carrier of S] -tree p) )
reconsider t = (Sym (o,X)) -tree p as Term of S,X ;
assume [o, the carrier of S] -tree p in the Sorts of (Free (S,X)) . s ; :: thesis: # (([o, the carrier of S] -tree p),w) = (h . s) . ([o, the carrier of S] -tree p)
then t in the Sorts of (FreeMSA X) . s by MSAFREE3:31;
then t in FreeSort (X,s) by MSAFREE:def 11;
then ( the_sort_of t = s & t . {} = Sym (o,X) ) by TREES_4:def 4, MSATERM:def 5;
then A12: s = the_result_sort_of o by MSATERM:17;
FreeMSA X = Free (S,X) by MSAFREE3:31;
then reconsider q = p as Element of Args (o,(Free (S,X))) by INSTALG1:1;
rng p c= dom F

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng p or y in dom F )
assume y in rng p ; :: thesis: y in dom F
then consider x being object such that
A13: ( x in dom p & y = p . x ) by FUNCT_1:def 3;
reconsider x = x as Nat by A13;
( p . x is Term of S,X & dom F = S -Terms X ) by A13, MSATERM:22, PARTFUN1:def 2;
hence y in dom F by A13; :: thesis: verum

end;

then A14: ( dom (F * p) = dom p & dom (h # q) = dom (the_arity_of o) & dom q = dom (the_arity_of o) ) by RELAT_1:27, MSUALG_3:6;

now :: thesis: for x being object st x in dom p holds
(F * p) . x = (h # q) . x

let x be object ; :: thesis: ( x in dom p implies (F * p) . x = (h # q) . x )
assume A15: x in dom p ; :: thesis: (F * p) . x = (h # q) . x
then reconsider i = x as Nat ;
reconsider t = p . i as Term of S,X by A15, MSATERM:22;
t is Element of (FreeMSA X) by MSATERM:13;
then reconsider u = t as Element of (Free (S,X)) by MSAFREE3:31;
reconsider s = (the_arity_of o) /. i as SortSymbol of S ;
A16: t in rng p by A15, FUNCT_1:def 3;
the_sort_of t = s by A15, MSATERM:23;
then t in FreeSort (X,s) by MSATERM:def 5;
then t in the Sorts of (FreeMSA X) . s by MSAFREE:def 11;
then A17: t in the Sorts of (Free (S,X)) . s by MSAFREE3:31;
thus (F * p) . x = F . t by A15, FUNCT_1:13
.= # (u,w) by A7, Th55
.= (h . s) . u by A11, A16, A17
.= (h # q) . x by A15, MSUALG_3:def 6 ; :: thesis: verum

end;

then A18: F * p = h # q by A14;
t is Element of (FreeMSA X) by MSATERM:13;
then t is Element of (Free (S,X)) by MSAFREE3:31;
hence # (([o, the carrier of S] -tree p),w) = F . t by Th55, A7
.= (Sym (o,( the carrier of S --> NAT))) -tree (F * p) by A7
.= (Den (o,(Free (S,( the carrier of S --> NAT))))) . (h # q) by A18, A1, Th13
.= (h . s) . ((Den (o,(Free (S,X)))) . q) by A1, A6, A12
.= (h . s) . ([o, the carrier of S] -tree p) by Th13 ;
:: thesis: verum

end;

A19: for t being Term of S,X holds S₁[t] from MSATERM:sch 1(A8, A10);
t is Element of the Sorts of (Free (S,X)) . s ;
then t is Element of (FreeMSA X) by MSAFREE3:31;
then t is Term of S,X by MSATERM:13;
hence # (t,w) = (h . s) . t by A19; :: thesis: verum