let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S
for V being Variables of A
for f being ManySortedFunction of V, the Sorts of A
for o being OperSymbol of S
for p being ArgumentSeq of o,A,V
for q being DTree-yielding FinSequence st len q = len p & ( 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 ) ) holds
ex vt being finite DecoratedTree st
( vt = ((Den (o,A)) . (roots q)) -tree q & vt is_an_evaluation_of (Sym (o,( the Sorts of A (\/) V))) -tree p,f )
let A be non-empty MSAlgebra over S; :: thesis: for V being Variables of A
for f being ManySortedFunction of V, the Sorts of A
for o being OperSymbol of S
for p being ArgumentSeq of o,A,V
for q being DTree-yielding FinSequence st len q = len p & ( 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 ) ) holds
ex vt being finite DecoratedTree st
( vt = ((Den (o,A)) . (roots q)) -tree q & vt is_an_evaluation_of (Sym (o,( the Sorts of A (\/) V))) -tree p,f )
let V be Variables of A; :: thesis: for f being ManySortedFunction of V, the Sorts of A
for o being OperSymbol of S
for p being ArgumentSeq of o,A,V
for q being DTree-yielding FinSequence st len q = len p & ( 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 ) ) holds
ex vt being finite DecoratedTree st
( vt = ((Den (o,A)) . (roots q)) -tree q & vt is_an_evaluation_of (Sym (o,( the Sorts of A (\/) V))) -tree p,f )
let f be ManySortedFunction of V, the Sorts of A; :: thesis: for o being OperSymbol of S
for p being ArgumentSeq of o,A,V
for q being DTree-yielding FinSequence st len q = len p & ( 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 ) ) holds
ex vt being finite DecoratedTree st
( vt = ((Den (o,A)) . (roots q)) -tree q & vt is_an_evaluation_of (Sym (o,( the Sorts of A (\/) V))) -tree p,f )
let o be OperSymbol of S; :: thesis: for p being ArgumentSeq of o,A,V
for q being DTree-yielding FinSequence st len q = len p & ( 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 ) ) holds
ex vt being finite DecoratedTree st
( vt = ((Den (o,A)) . (roots q)) -tree q & vt is_an_evaluation_of (Sym (o,( the Sorts of A (\/) V))) -tree p,f )
let p be ArgumentSeq of o,A,V; :: thesis: for q being DTree-yielding FinSequence st len q = len p & ( 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 ) ) holds
ex vt being finite DecoratedTree st
( vt = ((Den (o,A)) . (roots q)) -tree q & vt is_an_evaluation_of (Sym (o,( the Sorts of A (\/) V))) -tree p,f )
A1: Sym (o,( the Sorts of A (\/) V)) = [o, the carrier of S] by MSAFREE:def 9;
A2: dom (doms p) = dom p by TREES_3:37;
A3: tree (doms p) = dom ([o, the carrier of S] -tree p) by TREES_4:10;
A4: dom p = Seg (len p) by FINSEQ_1:def 3;
let q be DTree-yielding FinSequence; :: thesis: ( len q = len p & ( 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 ) ) implies ex vt being finite DecoratedTree st
( vt = ((Den (o,A)) . (roots q)) -tree q & vt is_an_evaluation_of (Sym (o,( the Sorts of A (\/) V))) -tree p,f ) )
assume that
A5: len q = len p and
A6: 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: ex vt being finite DecoratedTree st
( vt = ((Den (o,A)) . (roots q)) -tree q & vt is_an_evaluation_of (Sym (o,( the Sorts of A (\/) V))) -tree p,f )
A7: dom q = Seg (len q) by FINSEQ_1:def 3;

now :: thesis: for x being object st x in dom (doms q) holds
(doms q) . x is finite Tree

let x be object ; :: thesis: ( x in dom (doms q) implies (doms q) . x is finite Tree )
A8: rng p c= S -Terms ( the Sorts of A (\/) V) by FINSEQ_1:def 4;
assume A9: x in dom (doms q) ; :: thesis: (doms q) . x is finite Tree
then A10: x in dom q by TREES_3:37;
then p . x in rng p by A5, A4, A7, FUNCT_1:def 3;
then reconsider t = p . x as c-Term of A,V by A8;
reconsider i = x as Nat by A9;
consider vt being finite DecoratedTree such that
A11: vt = q . i and
vt is_an_evaluation_of t,f by A5, A6, A4, A7, A10;
(doms q) . x = dom vt by A10, A11, FUNCT_6:22;
hence (doms q) . x is finite Tree ; :: thesis: verum

end;

then reconsider r = doms q as FinTree-yielding FinSequence by TREES_3:23;

A12: now :: thesis: for i being Nat st i in dom p holds
r . i = (doms p) . i

let i be Nat; :: thesis: ( i in dom p implies r . i = (doms p) . i )
A13: rng p c= S -Terms ( the Sorts of A (\/) V) by FINSEQ_1:def 4;
assume A14: i in dom p ; :: thesis: r . i = (doms p) . i
then p . i in rng p by FUNCT_1:def 3;
then reconsider t = p . i as c-Term of A,V by A13;
consider vt being finite DecoratedTree such that
A15: vt = q . i and
A16: vt is_an_evaluation_of t,f by A6, A14;
thus r . i = dom vt by A5, A4, A7, A14, A15, FUNCT_6:22
.= dom t by A16
.= (doms p) . i by A14, FUNCT_6:22 ; :: thesis: verum

end;

set vt = ((Den (o,A)) . (roots q)) -tree q;
A17: len (doms q) = len q by TREES_3:38;
A18: dom (((Den (o,A)) . (roots q)) -tree q) = tree r by TREES_4:10;
then reconsider vt = ((Den (o,A)) . (roots q)) -tree q as finite DecoratedTree by FINSET_1:10;
take vt ; :: thesis: ( vt = ((Den (o,A)) . (roots q)) -tree q & vt is_an_evaluation_of (Sym (o,( the Sorts of A (\/) V))) -tree p,f )
thus vt = ((Den (o,A)) . (roots q)) -tree q ; :: thesis: vt is_an_evaluation_of (Sym (o,( the Sorts of A (\/) V))) -tree p,f
dom (doms q) = dom q by TREES_3:37;
hence dom vt = dom ((Sym (o,( the Sorts of A (\/) V))) -tree p) by A1, A5, A4, A7, A18, A3, A2, A12, FINSEQ_1:13; :: according to MSATERM:def 9 :: thesis: for p being Node of vt holds
( ( for s being SortSymbol of S
for v being Element of V . s st ((Sym (o,( the Sorts of A (\/) V))) -tree p) . p = [v,s] holds
vt . p = (f . s) . v ) & ( for s being SortSymbol of S
for x being Element of the Sorts of A . s st ((Sym (o,( the Sorts of A (\/) V))) -tree p) . p = [x,s] holds
vt . p = x ) & ( for o being OperSymbol of S st ((Sym (o,( the Sorts of A (\/) V))) -tree p) . p = [o, the carrier of S] holds
vt . p = (Den (o,A)) . (succ (vt,p)) ) )
let n be Node of vt; :: thesis: ( ( for s being SortSymbol of S
for v being Element of V . s st ((Sym (o,( the Sorts of A (\/) V))) -tree p) . n = [v,s] holds
vt . n = (f . s) . v ) & ( for s being SortSymbol of S
for x being Element of the Sorts of A . s st ((Sym (o,( the Sorts of A (\/) V))) -tree p) . n = [x,s] holds
vt . n = x ) & ( for o being OperSymbol of S st ((Sym (o,( the Sorts of A (\/) V))) -tree p) . n = [o, the carrier of S] holds
vt . n = (Den (o,A)) . (succ (vt,n)) ) )
A19: ([o, the carrier of S] -tree p) . {} = [o, the carrier of S] by TREES_4:def 4;

hereby :: thesis: ( ( for s being SortSymbol of S
for x being Element of the Sorts of A . s st ((Sym (o,( the Sorts of A (\/) V))) -tree p) . n = [x,s] holds
vt . n = x ) & ( for o being OperSymbol of S st ((Sym (o,( the Sorts of A (\/) V))) -tree p) . n = [o, the carrier of S] holds
vt . n = (Den (o,A)) . (succ (vt,n)) ) )

let s be SortSymbol of S; :: thesis: for v being Element of V . s st ((Sym (o,( the Sorts of A (\/) V))) -tree p) . n = [v,s] holds
vt . n = (f . s) . v
let v be Element of V . s; :: thesis: ( ((Sym (o,( the Sorts of A (\/) V))) -tree p) . n = [v,s] implies vt . n = (f . s) . v )
assume A20: ((Sym (o,( the Sorts of A (\/) V))) -tree p) . n = [v,s] ; :: thesis: vt . n = (f . s) . v

now :: thesis: not n = {}

assume n = {} ; :: thesis: contradiction
then s = the carrier of S by A1, A19, A20, XTUPLE_0:1;
hence contradiction by Lm7; :: thesis: verum

end;

then consider w being FinSequence of NAT , i being Element of NAT such that
A21: n = <*i*> ^ w by FINSEQ_2:130;
A22: w in (doms q) . (i + 1) by A18, A21, TREES_3:48;
A23: i < len p by A5, A18, A17, A21, TREES_3:48;
then reconsider t = p . (i + 1) as c-Term of A,V by Lm2;
consider e being finite DecoratedTree such that
A24: e = q . (i + 1) and
A25: e is_an_evaluation_of t,f by A6, A23, Lm9;
i + 1 in dom p by A23, Lm9;
then reconsider w = w as Node of e by A5, A4, A7, A22, A24, FUNCT_6:22;
dom e = dom t by A25;
then A26: t . w = [v,s] by A20, A21, A23, TREES_4:12;
thus vt . n = e . w by A5, A21, A23, A24, TREES_4:12
.= (f . s) . v by A25, A26 ; :: thesis: verum

end;

hereby :: thesis: for o being OperSymbol of S st ((Sym (o,( the Sorts of A (\/) V))) -tree p) . n = [o, the carrier of S] holds
vt . n = (Den (o,A)) . (succ (vt,n))

let s be SortSymbol of S; :: thesis: for x being Element of the Sorts of A . s st ((Sym (o,( the Sorts of A (\/) V))) -tree p) . n = [x,s] holds
vt . n = x
let x be Element of the Sorts of A . s; :: thesis: ( ((Sym (o,( the Sorts of A (\/) V))) -tree p) . n = [x,s] implies vt . n = x )
assume A27: ((Sym (o,( the Sorts of A (\/) V))) -tree p) . n = [x,s] ; :: thesis: vt . n = x

now :: thesis: not n = {}

assume n = {} ; :: thesis: contradiction
then s = the carrier of S by A1, A19, A27, XTUPLE_0:1;
hence contradiction by Lm7; :: thesis: verum

end;

then consider w being FinSequence of NAT , i being Element of NAT such that
A28: n = <*i*> ^ w by FINSEQ_2:130;
A29: w in (doms q) . (i + 1) by A18, A28, TREES_3:48;
A30: i < len p by A5, A18, A17, A28, TREES_3:48;
then reconsider t = p . (i + 1) as c-Term of A,V by Lm2;
consider e being finite DecoratedTree such that
A31: e = q . (i + 1) and
A32: e is_an_evaluation_of t,f by A6, A30, Lm9;
i + 1 in dom p by A30, Lm9;
then reconsider w = w as Node of e by A5, A4, A7, A29, A31, FUNCT_6:22;
dom e = dom t by A32;
then A33: t . w = [x,s] by A27, A28, A30, TREES_4:12;
thus vt . n = e . w by A5, A28, A30, A31, TREES_4:12
.= x by A32, A33 ; :: thesis: verum

end;

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

per cases ( n = {} or n <> {} ) ;

suppose A35: n = {} ; :: thesis: vt . n = (Den (o1,A)) . (succ (vt,n))

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 9 ;
then A36: o = o1 by A34, XTUPLE_0:1;
succ (vt,n) = roots q by A35, TREES_9:30;
hence vt . n = (Den (o1,A)) . (succ (vt,n)) by A35, A36, TREES_4:def 4; :: thesis: verum

end;

suppose n <> {} ; :: thesis: vt . n = (Den (o1,A)) . (succ (vt,n))

then consider w being FinSequence of NAT , i being Element of NAT such that
A37: n = <*i*> ^ w by FINSEQ_2:130;
reconsider ii = <*i*> as Node of vt by A37, TREES_1:21;
A38: w in (doms q) . (i + 1) by A18, A37, TREES_3:48;
A39: i < len p by A5, A18, A17, A37, TREES_3:48;
then reconsider t = p . (i + 1) as c-Term of A,V by Lm2;
consider e being finite DecoratedTree such that
A40: e = q . (i + 1) and
A41: e is_an_evaluation_of t,f by A6, A39, Lm9;
A42: e = vt | ii by A5, A39, A40, TREES_4:def 4;
i + 1 in dom p by A39, Lm9;
then reconsider w = w as Node of e by A5, A4, A7, A38, A40, FUNCT_6:22;
dom e = dom t by A41;
then t . w = [o1, the carrier of S] by A34, A37, A39, TREES_4:12;
then e . w = (Den (o1,A)) . (succ (e,w)) by A41
.= (Den (o1,A)) . (succ (vt,n)) by A37, A42, TREES_9:31 ;
hence vt . n = (Den (o1,A)) . (succ (vt,n)) by A5, A37, A39, A40, TREES_4:12; :: thesis: verum

end;

end;