let S be non empty non void ManySortedSign ; :: thesis:
let A be non-empty MSAlgebra of S; :: thesis:
let V be Variables of A; :: thesis:
let f be ManySortedFunction of V,the Sorts of A; :: thesis:
let o be OperSymbol of S; :: thesis:
let p be ArgumentSeq of o,A,V; :: thesis:
A1: Sym o,(the Sorts of A \/ V) = [o,the carrier of S] by MSAFREE:def 11;
let q be DTree-yielding FinSequence; :: thesis:
assume that
A2: len q = len p and
A3: for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) ; :: thesis:
A4: ( dom p = Seg (len p) & dom q = Seg (len q) ) by FINSEQ_1:def 3;

now

let x be set ; :: thesis:
assume A5: x in dom (doms q) ; :: thesis:
then A6: x in dom q by TREES_3:39;
then ( p . x in rng p & rng p c= S -Terms (the Sorts of A \/ V) ) by A2, A4, FINSEQ_1:def 4, FUNCT_1:def 5;
then reconsider t = p . x as c-Term of A,V ;
reconsider i = x as Nat by A5;
consider vt being finite DecoratedTree such that
A7: ( vt = q . i & vt is_an_evaluation_of t,f ) by A2, A3, A4, A6;
(doms q) . x = dom vt by A6, A7, FUNCT_6:31;
hence (doms q) . x is finite Tree ; :: thesis:

end;

then reconsider r = doms q as FinTree-yielding FinSequence by TREES_3:25;
set vt = ((Den o,A) . (roots q)) -tree q;
A8: ( dom (((Den o,A) . (roots q)) -tree q) = tree r & tree (doms p) = dom ([o,the carrier of S] -tree p) ) by TREES_4:10;
then reconsider vt = ((Den o,A) . (roots q)) -tree q as finite DecoratedTree by FINSET_1:29;
take vt ; :: thesis:
thus vt = ((Den o,A) . (roots q)) -tree q ; :: thesis:
A9: ( dom (doms p) = dom p & len (doms p) = len p & dom (doms q) = dom q & len (doms q) = len q ) by TREES_3:39, TREES_3:40;

now

let i be Nat; :: thesis:
assume A10: i in dom p ; :: thesis:
then ( p . i in rng p & rng p c= S -Terms (the Sorts of A \/ V) ) by FINSEQ_1:def 4, FUNCT_1:def 5;
then reconsider t = p . i as c-Term of A,V ;
consider vt being finite DecoratedTree such that
A11: ( vt = q . i & vt is_an_evaluation_of t,f ) by A3, A10;
thus r . i = dom vt by A2, A4, A10, A11, FUNCT_6:31
.= dom t by A11, Def9
.= (doms p) . i by A10, FUNCT_6:31 ; :: thesis:

end;

hence dom vt = dom ((Sym o,(the Sorts of A \/ V)) -tree p) by A1, A2, A4, A8, A9, FINSEQ_1:17; :: according to MSATERM:def 9 :: thesis:
let n be Node of vt; :: thesis:
A12: ([o,the carrier of S] -tree p) . {} = [o,the carrier of S] by TREES_4:def 4;

hereby :: thesis:

let s be SortSymbol of S; :: thesis:
let v be Element of V . s; :: thesis:
assume A13: ((Sym o,(the Sorts of A \/ V)) -tree p) . n = [v,s] ; :: thesis:

now

assume n = {} ; :: thesis:
then s = the carrier of S by A1, A12, A13, ZFMISC_1:33;
hence contradiction by Lm7; :: thesis:

end;

then consider w being FinSequence of NAT , i being Nat such that
A14: n = <*i*> ^ w by MODAL_1:4;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
A15: ( i < len p & w in (doms q) . (i + 1) ) by A2, A8, A9, A14, TREES_3:51;
then reconsider t = p . (i + 1) as c-Term of A,V by Lm2;
A16: i + 1 in dom p by A15, Lm9;
then consider e being finite DecoratedTree such that
A17: ( e = q . (i + 1) & e is_an_evaluation_of t,f ) by A3;
A18: ( dom e = dom t & dom e = (doms q) . (i + 1) ) by A2, A4, A16, A17, Def9, FUNCT_6:31;
reconsider w = w as Node of e by A2, A4, A15, A16, A17, FUNCT_6:31;
A19: t . w = [v,s] by A13, A14, A15, A18, TREES_4:12;
thus vt . n = e . w by A2, A14, A15, A17, TREES_4:12
.= (f . s) . v by A17, A19, Def9 ; :: thesis:

end;

hereby :: thesis:

let s be SortSymbol of S; :: thesis:
let x be Element of the Sorts of A . s; :: thesis:
assume A20: ((Sym o,(the Sorts of A \/ V)) -tree p) . n = [x,s] ; :: thesis:

now

assume n = {} ; :: thesis:
then s = the carrier of S by A1, A12, A20, ZFMISC_1:33;
hence contradiction by Lm7; :: thesis:

end;

then consider w being FinSequence of NAT , i being Nat such that
A21: n = <*i*> ^ w by MODAL_1:4;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
A22: ( i < len p & w in (doms q) . (i + 1) ) by A2, A8, A9, A21, TREES_3:51;
then reconsider t = p . (i + 1) as c-Term of A,V by Lm2;
A23: i + 1 in dom p by A22, Lm9;
then consider e being finite DecoratedTree such that
A24: ( e = q . (i + 1) & e is_an_evaluation_of t,f ) by A3;
A25: ( dom e = dom t & dom e = (doms q) . (i + 1) ) by A2, A4, A23, A24, Def9, FUNCT_6:31;
reconsider w = w as Node of e by A2, A4, A22, A23, A24, FUNCT_6:31;
A26: t . w = [x,s] by A20, A21, A22, A25, TREES_4:12;
thus vt . n = e . w by A2, A21, A22, A24, TREES_4:12
.= x by A24, A26, Def9 ; :: thesis:

end;

let o1 be OperSymbol of S; :: thesis:
assume A27: ((Sym o,(the Sorts of A \/ V)) -tree p) . n = [o1,the carrier of S] ; :: thesis:

per cases ;

suppose A28: n = {} ; :: thesis:

then ((Sym o,(the Sorts of A \/ V)) -tree p) . n = Sym o,(the Sorts of A \/ V) by TREES_4:def 4
.= [o,the carrier of S] by MSAFREE:def 11 ;
then ( o = o1 & succ vt,n = roots q ) by A27, A28, TREES_9:31, ZFMISC_1:33;
hence vt . n = (Den o1,A) . (succ vt,n) by A28, TREES_4:def 4; :: thesis:

end;

suppose n <> {} ; :: thesis:

then consider w being FinSequence of NAT , i being Nat such that
A29: n = <*i*> ^ w by MODAL_1:4;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
A30: ( i < len p & w in (doms q) . (i + 1) ) by A2, A8, A9, A29, TREES_3:51;
then reconsider t = p . (i + 1) as c-Term of A,V by Lm2;
A31: i + 1 in dom p by A30, Lm9;
then consider e being finite DecoratedTree such that
A32: ( e = q . (i + 1) & e is_an_evaluation_of t,f ) by A3;
A33: ( dom e = dom t & dom e = (doms q) . (i + 1) ) by A2, A4, A31, A32, Def9, FUNCT_6:31;
reconsider w = w as Node of e by A2, A4, A30, A31, A32, FUNCT_6:31;
reconsider ii = <*i*> as Node of vt by A29, TREES_1:46;
A34: e = vt | ii by A2, A30, A32, TREES_4:def 4;
t . w = [o1,the carrier of S] by A27, A29, A30, A33, TREES_4:12;
then e . w = (Den o1,A) . (succ e,w) by A32, Def9
.= (Den o1,A) . (succ vt,n) by A29, A34, TREES_9:32 ;
hence vt . n = (Den o1,A) . (succ vt,n) by A2, A29, A30, A32, TREES_4:12; :: thesis:

end;