let S be non empty non void ManySortedSign ; :: thesis:
let X0 be non-empty countable ManySortedSet of S; :: thesis:
let A0 be X0,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; :: thesis:
set A = A0;
let w be ManySortedFunction of X0, the carrier of S --> NAT; :: thesis:
let s be SortSymbol of S; :: thesis:
set k = canonical_homomorphism A0;
set Y = the carrier of S --> NAT;
defpred S₁[ DecoratedTree-like Function] means for s being SortSymbol of S
for t1, t2 being Element of (TermAlg S),s
for t3 being Term of S,X0 st t3 = ((canonical_homomorphism A0) . s) . $1 & t1 = # ($1,w) & t2 = # (t3,w) holds
A0 |= t1 '=' t2;
A1: for s1 being SortSymbol of S
for v being Element of X0 . s1 holds S₁[ root-tree [v,s1]]

proof

let s1 be SortSymbol of S; :: thesis:
let v be Element of X0 . s1; :: thesis:
set t = root-tree [v,s1];
let s be SortSymbol of S; :: thesis:
let t1, t2 be Element of (TermAlg S),s; :: thesis:
let t3 be Term of S,X0; :: thesis:
assume A2: t3 = ((canonical_homomorphism A0) . s) . (root-tree [v,s1]) ; :: thesis:
assume A3: t1 = # ((root-tree [v,s1]),w) ; :: thesis:
assume A4: t2 = # (t3,w) ; :: thesis:
( t1 = root-tree [((w . s1) . v),s1] & FreeMSA ( the carrier of S --> NAT) = Free (S,( the carrier of S --> NAT)) ) by A3, Th57, MSAFREE3:31;
then ( t1 in the Sorts of (Free (S,( the carrier of S --> NAT))) . s1 & t1 in the Sorts of (Free (S,( the carrier of S --> NAT))) . s ) by MSAFREE3:4;
then ( the Sorts of (Free (S,( the carrier of S --> NAT))) . s1 meets the Sorts of (Free (S,( the carrier of S --> NAT))) . s & ( s <> s1 implies the Sorts of (Free (S,( the carrier of S --> NAT))) . s1 misses the Sorts of (Free (S,( the carrier of S --> NAT))) . s ) ) by XBOOLE_0:3, PROB_2:def 2;
then root-tree [v,s1] is Element of A0,s by Th40;
then t3 = root-tree [v,s1] by A2, Th47;
hence A0 |= t1 '=' t2 by A3, A4; :: thesis:

end;

A5: 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 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:
let t1, t2 be Element of (TermAlg S),s; :: thesis:
let t3 be Term of S,X0; :: thesis:
assume A6: t3 = ((canonical_homomorphism A0) . s) . ([o, the carrier of S] -tree p) ; :: thesis:
assume A7: t1 = # (([o, the carrier of S] -tree p),w) ; :: thesis:
assume A8: t2 = # (t3,w) ; :: thesis:
A9: FreeMSA X0 = Free (S,X0) by MSAFREE3:31;
then reconsider a = p as Element of Args (o,(Free (S,X0))) by INSTALG1:1;
A10: [o, the carrier of S] -tree p = (Den (o,(Free (S,X0)))) . a by A9, INSTALG1:3;
t1 is Element of the Sorts of (Free (S,( the carrier of S --> NAT))) . s by MSAFREE3:31;
then reconsider tq = t1 as Term of S,( the carrier of S --> NAT) by Th42;
defpred S₂[ Nat, object ] means for t being Element of (Free (S,X0)) st t = p . $1 holds
$2 = # (t,w);
A11: dom p = Seg (len p) by FINSEQ_1:def 3;
A12: 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 A11, 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
A13: ( 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(A12);
( 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 A11, A13;
then A14: t1 = (Sym (o,( the carrier of S --> NAT))) -tree q by A7, Th58;

now :: thesis:

let i be object ; :: thesis:
assume A15: i in dom q ; :: thesis:
then p . i is Term of S,X0 by A11, A13, 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 A13, A15;
then q . i is Element of (Free (S,( the carrier of S --> NAT))) by MSAFREE3:31;
hence q . i is DecoratedTree ; :: thesis:

end;

then q is DTree-yielding by TREES_3:24;
then tq . {} = Sym (o,( the carrier of S --> NAT)) by A14, TREES_4:def 4;
then the_sort_of tq = the_result_sort_of o by MSATERM:17;
then tq in FreeSort (( the carrier of S --> NAT),(the_result_sort_of o)) by MSATERM:def 5;
then ( t1 in the Sorts of (TermAlg S) . s & t1 in the Sorts of (TermAlg S) . (the_result_sort_of o) ) by MSAFREE:def 11;
then A16: s = the_result_sort_of o by PROB_2:def 2, XBOOLE_0:3;
reconsider tt = [o, the carrier of S] -tree p as Element of (Free (S,X0)),s by A16, A10, MSUALG_9:18;
A17: the Sorts of A0 is MSSubset of (Free (S,X0)) by Def6;
( ((canonical_homomorphism A0) . s) . tt in the Sorts of A0 . s & the Sorts of A0 . s c= the Sorts of (Free (S,X0)) . s ) by A17, PBOOLE:def 2, PBOOLE:def 18;
then reconsider kt = ((canonical_homomorphism A0) . s) . tt as Element of (Free (S,X0)),s ;
let h be ManySortedFunction of (TermAlg S),A0; :: according to EQUATION:def 5 :: thesis:
assume A18: h is_homomorphism TermAlg S,A0 ; :: thesis:
consider hh being ManySortedFunction of (Free (S,X0)),(TermAlg S) such that
A19: ( hh is_homomorphism Free (S,X0), TermAlg S & ( for s being SortSymbol of S
for t being Element of (Free (S,X0)),s holds # (t,w) = (hh . s) . t ) ) by Th56;
A20: ( ((canonical_homomorphism A0) . s) . ((Den (o,(Free (S,X0)))) . a) in the Sorts of A0 . s & the Sorts of A0 . s c= the Sorts of (Free (S,X0)) . s ) by A17, PBOOLE:def 2, PBOOLE:def 18, FUNCT_2:5, A16, MSUALG_9:18;
thus (h . s) . ((t1 '=' t2) `1) = (h . s) . ((hh . s) . tt) by A7, A19
.= (h . s) . ((hh . s) . ((Den (o,(Free (S,X0)))) . a)) by A9, INSTALG1:3
.= ((h . s) * (hh . s)) . ((Den (o,(Free (S,X0)))) . a) by A16, MSUALG_9:18, FUNCT_2:15
.= ((h ** hh) . s) . ((Den (o,(Free (S,X0)))) . a) by MSUALG_3:2
.= ((h ** hh) . s) . ((Den (o,(Free (S,X0)))) . ((canonical_homomorphism A0) # a)) by A16, Th69, A18, A19, MSUALG_3:10
.= ((h ** hh) . s) . ((Den (o,A0)) . ((canonical_homomorphism A0) # a)) by Th68, A18, A19, MSUALG_3:10, A16
.= ((h ** hh) . s) . (((canonical_homomorphism A0) . s) . ((Den (o,(Free (S,X0)))) . a)) by A16, Def10, MSUALG_3:def 7
.= ((h . s) * (hh . s)) . (((canonical_homomorphism A0) . s) . ((Den (o,(Free (S,X0)))) . a)) by MSUALG_3:2
.= (h . s) . ((hh . s) . (((canonical_homomorphism A0) . s) . ((Den (o,(Free (S,X0)))) . a))) by A20, FUNCT_2:15
.= (h . s) . ((hh . s) . kt) by A9, INSTALG1:3
.= (h . s) . t2 by A6, A8, A19
.= (h . s) . ((t1 '=' t2) `2) ; :: thesis:

end;

A21: for t being Term of S,X0 holds S₁[t] from MSATERM:sch 1(A1, A5);
let t be Element of the Sorts of (Free (S,X0)) . s; :: thesis:
A22: t is Term of S,X0 by Th42;
let t1, t2 be Element of (TermAlg S),s; :: thesis:
assume A23: t1 = # (t,w) ; :: thesis:
assume A24: t2 = # ((((canonical_homomorphism A0) . s) . t),w) ; :: thesis:
((canonical_homomorphism A0) . s) . t is Element of the Sorts of A0 . s ;
then ((canonical_homomorphism A0) . s) . t is Term of S,X0 by Th42;
hence A0 |= t1 '=' t2 by A22, A21, A23, A24; :: thesis: