let S be non empty non void ManySortedSign ; :: thesis:
let X0 be non-empty countable ManySortedSet of S; :: thesis:
let w be ManySortedFunction of X0, the carrier of S --> NAT; :: thesis:
assume A1: w is "1-1" ; :: thesis:
A2: Free (S,X0) = FreeMSA X0 by MSAFREE3:31;
reconsider G = FreeGen ( the carrier of S --> NAT) as non-empty GeneratorSet of TermAlg S ;
set Y = the carrier of S --> NAT;
defpred S₁[ set , set , set ] means for x being Element of ( the carrier of S --> NAT) . $1 st $2 = root-tree [x,$1] holds
( ( x in rng (w . $1) implies $3 = root-tree [(((w . $1) ") . x),$1] ) & ( x nin rng (w . $1) implies $3 = the Element of the Sorts of (Free (S,X0)) . $1 ) );
A3: for s being SortSymbol of S
for t being Element of G . s ex T being Element of the Sorts of (Free (S,X0)) . s st S₁[s,t,T]

proof

let s be SortSymbol of S; :: thesis:
let t be Element of G . s; :: thesis:
t in G . s ;
then t in FreeGen (s,( the carrier of S --> NAT)) by MSAFREE:def 16;
then consider x being set such that
A4: ( x in ( the carrier of S --> NAT) . s & t = root-tree [x,s] ) by MSAFREE:def 15;
reconsider x = x as Element of ( the carrier of S --> NAT) . s by A4;

per cases ;

suppose A5: x in rng (w . s) ; :: thesis:

then consider a being object such that
A6: ( a in dom (w . s) & x = (w . s) . a ) by FUNCT_1:def 3;
reconsider T = root-tree [a,s] as Element of the Sorts of (Free (S,X0)) . s by A6, MSAFREE3:4;
take T ; :: thesis:
let x0 be Element of ( the carrier of S --> NAT) . s; :: thesis:
assume t = root-tree [x0,s] ; :: thesis:
then A7: [x0,s] = [x,s] by A4, TREES_4:4;
then A8: x = x0 by XTUPLE_0:1;
w . s is one-to-one by A1, MSUALG_3:1;
hence ( x0 in rng (w . s) implies T = root-tree [(((w . s) ") . x0),s] ) by A6, A8, FUNCT_1:34; :: thesis:
thus ( x0 nin rng (w . s) implies T = the Element of the Sorts of (Free (S,X0)) . s ) by A5, A7, XTUPLE_0:1; :: thesis:

end;

suppose A9: x nin rng (w . s) ; :: thesis:

set T = the Element of the Sorts of (Free (S,X0)) . s;
take the Element of the Sorts of (Free (S,X0)) . s ; :: thesis:
let x0 be Element of ( the carrier of S --> NAT) . s; :: thesis:
assume t = root-tree [x0,s] ; :: thesis:
then [x0,s] = [x,s] by A4, TREES_4:4;
hence ( ( x0 in rng (w . s) implies the Element of the Sorts of (Free (S,X0)) . s = root-tree [(((w . s) ") . x0),s] ) & ( x0 nin rng (w . s) implies the Element of the Sorts of (Free (S,X0)) . s = the Element of the Sorts of (Free (S,X0)) . s ) ) by A9, XTUPLE_0:1; :: thesis:

end;

consider gg being ManySortedFunction of G, the Sorts of (Free (S,X0)) such that
A10: for s being SortSymbol of S
for t being Element of G . s holds S₁[s,t,(gg . s) . t] from CIRCTRM1:sch 1(A3);
consider g being ManySortedFunction of (TermAlg S),(Free (S,X0)) such that
A11: ( g is_homomorphism TermAlg S, Free (S,X0) & g || G = gg ) by MSAFREE:def 5;
take g ; :: thesis:
thus g is_homomorphism TermAlg S, Free (S,X0) by A11; :: thesis:
defpred S₂[ DecoratedTree] means for s being SortSymbol of S st $1 in the Sorts of (Free (S,X0)) . s holds
(g . s) . (# ($1,w)) = $1;
A12: for s being SortSymbol of S
for v being Element of X0 . s holds S₂[ root-tree [v,s]]

proof

let s be SortSymbol of S; :: thesis:
let v be Element of X0 . s; :: thesis:
set t = root-tree [v,s];
let s0 be SortSymbol of S; :: thesis:
assume A13: root-tree [v,s] in the Sorts of (Free (S,X0)) . s0 ; :: thesis:
root-tree [v,s] in the Sorts of (Free (S,X0)) . s by MSAFREE3:4;
then A14: s = s0 by A13, XBOOLE_0:3, PROB_2:def 2;
then A15: ( (w . s0) . v in rng (w . s0) & (w . s0) . v in ( the carrier of S --> NAT) . s0 ) by FUNCT_2:4, FUNCT_2:5;
then root-tree [((w . s0) . v),s0] in FreeGen (s0,( the carrier of S --> NAT)) by MSAFREE:def 15;
then A16: root-tree [((w . s0) . v),s0] in G . s0 by MSAFREE:def 16;
then A17: (gg . s0) . (root-tree [((w . s0) . v),s0]) = root-tree [(((w . s0) ") . ((w . s0) . v)),s0] by A15, A10;
A18: # ((root-tree [v,s]),w) = root-tree [((w . s0) . v),s0] by A14, Th57;
gg . s0 = (g . s0) | (G . s0) by A11, MSAFREE:def 1;
then A19: (g . s0) . (root-tree [((w . s0) . v),s0]) = root-tree [(((w . s0) ") . ((w . s0) . v)),s0] by A16, A17, FUNCT_1:49;
w . s0 is one-to-one by A1, MSUALG_3:1;
hence (g . s0) . (# ((root-tree [v,s]),w)) = root-tree [v,s] by A14, A18, A19, FUNCT_2:26; :: thesis:

end;

A20: for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X0) st ( for t being Term of S,X0 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:
let p be ArgumentSeq of Sym (o,X0); :: thesis:
assume A21: for t being Term of S,X0 st t in rng p holds
S₂[t] ; :: thesis:
set t = [o, the carrier of S] -tree p;
let s be SortSymbol of S; :: thesis:
assume A22: [o, the carrier of S] -tree p in the Sorts of (Free (S,X0)) . s ; :: thesis:
([o, the carrier of S] -tree p) . {} = [o, the carrier of S] by TREES_4:def 4;
then the_sort_of ((Sym (o,X0)) -tree p) = the_result_sort_of o by MSATERM:17;
then [o, the carrier of S] -tree p in FreeSort (X0,(the_result_sort_of o)) by MSATERM:def 5;
then [o, the carrier of S] -tree p in the Sorts of (Free (S,X0)) . (the_result_sort_of o) by A2, MSAFREE:def 11;
then A23: s = the_result_sort_of o by A22, XBOOLE_0:3, PROB_2:def 2;
defpred S₃[ Nat, object ] means for t being Element of (Free (S,X0)) st t = p . $1 holds
$2 = # (t,w);
A24: dom p = Seg (len p) by FINSEQ_1:def 3;
A25: for i being Nat st i in Seg (len p) holds
ex x being object st S₃[i,x]

proof

let i be Nat; :: thesis:
assume i in Seg (len p) ; :: thesis:
then p . i is Term of S,X0 by A24, MSATERM:22;
then p . i is Element of (FreeMSA X0) by MSATERM:13;
then reconsider t = p . i as Element of (Free (S,X0)) by MSAFREE3:31;
take x = # (t,w); :: thesis:
thus S₃[i,x] ; :: thesis:

end;

consider q being FinSequence such that
A26: ( dom q = Seg (len p) & ( for i being Nat st i in Seg (len p) holds
S₃[i,q . i] ) ) from FINSEQ_1:sch 1(A25);
( dom q = dom p & ( for i being Nat
for t being Element of (Free (S,X0)) st i in dom p & t = p . i holds
q . i = # (t,w) ) ) by A24, A26;
then A27: # (([o, the carrier of S] -tree p),w) = (Sym (o,( the carrier of S --> NAT))) -tree q by Th58;

now :: thesis:

let i be object ; :: thesis:
assume A28: i in dom q ; :: thesis:
then p . i is Term of S,X0 by A24, A26, MSATERM:22;
then p . i is Element of (FreeMSA X0) by MSATERM:13;
then reconsider t = p . i as Element of (Free (S,X0)) by MSAFREE3:31;
q . i = # (t,w) by A26, A28;
then q . i is Element of (Free (S,( the carrier of S --> NAT))) by MSAFREE3:31;
hence q . i is DecoratedTree ; :: thesis:

end;

then A29: q is DTree-yielding by TREES_3:24;
TermAlg S = Free (S,( the carrier of S --> NAT)) by MSAFREE3:31;
then ( (# (([o, the carrier of S] -tree p),w)) . {} = Sym (o,( the carrier of S --> NAT)) & # (([o, the carrier of S] -tree p),w) is Term of S,( the carrier of S --> NAT) ) by Th42, A29, A27, TREES_4:def 4;
then consider r being ArgumentSeq of Sym (o,( the carrier of S --> NAT)) such that
A30: # (([o, the carrier of S] -tree p),w) = [o, the carrier of S] -tree r by MSATERM:10;
r = q by A29, A27, A30, TREES_4:15;
then reconsider q = q as Element of Args (o,(TermAlg S)) by INSTALG1:1;
reconsider a = p as Element of Args (o,(Free (S,X0))) by A2, INSTALG1:1;
for n being Nat st n in dom q holds
a . n = (g . ((the_arity_of o) /. n)) . (q . n)

proof

let n be Nat; :: thesis:
assume A31: n in dom q ; :: thesis:
A32: ( dom q = dom (the_arity_of o) & dom a = dom (the_arity_of o) ) by MSUALG_3:6;
then reconsider tn = a . n as Term of S,X0 by A31, MSATERM:22;
A33: tn in rng p by A31, A32, FUNCT_1:def 3;
the_sort_of tn = (the_arity_of o) /. n by A31, A32, MSATERM:23;
then tn in FreeSort (X0,((the_arity_of o) /. n)) by MSATERM:def 5;
then tn in the Sorts of (Free (S,X0)) . ((the_arity_of o) /. n) by A2, MSAFREE:def 11;
then A34: (g . ((the_arity_of o) /. n)) . (# (tn,w)) = tn by A21, A33;
( S₃[n,q . n] & tn is Element of (Free (S,X0)) ) by A2, A26, A31, MSATERM:13;
hence a . n = (g . ((the_arity_of o) /. n)) . (q . n) by A34; :: thesis:

end;

then A35: g # q = a by MSUALG_3:def 6;
thus (g . s) . (# (([o, the carrier of S] -tree p),w)) = (g . s) . ((Den (o,(TermAlg S))) . q) by A27, INSTALG1:3
.= (Den (o,(Free (S,X0)))) . (g # q) by A11, A23
.= [o, the carrier of S] -tree p by A2, A35, INSTALG1:3 ; :: thesis:

end;

A36: for t being Term of S,X0 holds S₂[t] from MSATERM:sch 1(A12, A20);
let s be SortSymbol of S; :: thesis:
let t be Element of the Sorts of (Free (S,X0)) . s; :: thesis:
t is Term of S,X0 by Th42;
hence (g . s) . (# (t,w)) = t by A36; :: thesis: