let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of 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 of 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 11;
A2: dom (doms p) = dom p by TREES_3:39;
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

let x be set ; :: 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:39;
then p . x in rng p by A5, A4, A7, FUNCT_1:def 5;
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:31;
hence (doms q) . x is finite Tree ; :: thesis: verum

end;

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

A12: now

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 5;
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:31
.= dom t by A16, Def9
.= (doms p) . i by A14, FUNCT_6:31 ; :: thesis: verum

end;

set vt = ((Den o,A) . (roots q)) -tree q;
A17: len (doms q) = len q by TREES_3:40;
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:29;
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:39;
hence dom vt = dom ((Sym o,(the Sorts of A \/ V)) -tree p) by A1, A5, A4, A7, A18, A3, A2, A12, FINSEQ_1:17; :: 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

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

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: w in (doms q) . (i + 1) by A18, A21, TREES_3:51;
A23: i < len p by A5, A18, A17, A21, TREES_3:51;
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:31;
dom e = dom t by A25, Def9;
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, Def9 ; :: 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

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

end;

then consider w being FinSequence of NAT , i being Nat such that
A28: n = <*i*> ^ w by MODAL_1:4;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
A29: w in (doms q) . (i + 1) by A18, A28, TREES_3:51;
A30: i < len p by A5, A18, A17, A28, TREES_3:51;
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:31;
dom e = dom t by A32, Def9;
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, Def9 ; :: 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 11 ;
then A36: o = o1 by A34, ZFMISC_1:33;
succ vt,n = roots q by A35, TREES_9:31;
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 Nat such that
A37: n = <*i*> ^ w by MODAL_1:4;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
reconsider ii = <*i*> as Node of vt by A37, TREES_1:46;
A38: w in (doms q) . (i + 1) by A18, A37, TREES_3:51;
A39: i < len p by A5, A18, A17, A37, TREES_3:51;
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:31;
dom e = dom t by A41, Def9;
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, Def9
.= (Den o1,A) . (succ vt,n) by A37, A42, TREES_9:32 ;
hence vt . n = (Den o1,A) . (succ vt,n) by A5, A37, A39, A40, TREES_4:12; :: thesis: verum

end;

end;