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 FinSequence st len q = len p & ( for i being Nat st i in dom p holds
for t being c-Term of A,V st t = p . i holds
q . i = t @ f ) holds
((Sym o,(the Sorts of A \/ V)) -tree p) @ f = (Den o,A) . q
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 FinSequence st len q = len p & ( for i being Nat st i in dom p holds
for t being c-Term of A,V st t = p . i holds
q . i = t @ f ) holds
((Sym o,(the Sorts of A \/ V)) -tree p) @ f = (Den o,A) . q
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 FinSequence st len q = len p & ( for i being Nat st i in dom p holds
for t being c-Term of A,V st t = p . i holds
q . i = t @ f ) holds
((Sym o,(the Sorts of A \/ V)) -tree p) @ f = (Den o,A) . q
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 FinSequence st len q = len p & ( for i being Nat st i in dom p holds
for t being c-Term of A,V st t = p . i holds
q . i = t @ f ) holds
((Sym o,(the Sorts of A \/ V)) -tree p) @ f = (Den o,A) . q
let o be OperSymbol of S; :: thesis: for p being ArgumentSeq of o,A,V
for q being FinSequence st len q = len p & ( for i being Nat st i in dom p holds
for t being c-Term of A,V st t = p . i holds
q . i = t @ f ) holds
((Sym o,(the Sorts of A \/ V)) -tree p) @ f = (Den o,A) . q
let p be ArgumentSeq of o,A,V; :: thesis: for q being FinSequence st len q = len p & ( for i being Nat st i in dom p holds
for t being c-Term of A,V st t = p . i holds
q . i = t @ f ) holds
((Sym o,(the Sorts of A \/ V)) -tree p) @ f = (Den o,A) . q
let q be FinSequence; :: thesis: ( len q = len p & ( for i being Nat st i in dom p holds
for t being c-Term of A,V st t = p . i holds
q . i = t @ f ) implies ((Sym o,(the Sorts of A \/ V)) -tree p) @ f = (Den o,A) . q )
assume that
A1: len q = len p and
A2: for i being Nat st i in dom p holds
for t being c-Term of A,V st t = p . i holds
q . i = t @ f ; :: thesis: ((Sym o,(the Sorts of A \/ V)) -tree p) @ f = (Den o,A) . q
consider vt being finite DecoratedTree such that
A3: vt is_an_evaluation_of (Sym o,(the Sorts of A \/ V)) -tree p,f by Th36;
consider r being DTree-yielding FinSequence such that
A4: len r = len p and
A5: vt = ((Den o,A) . (roots r)) -tree r 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 = r . i & vt is_an_evaluation_of t,f ) by A3, Th35;

now

thus A7: ( dom p = dom p & dom q = dom p & dom r = dom p ) by A1, A4, FINSEQ_3:31; :: thesis: for i being Element of NAT st i in dom r holds
ex T being DecoratedTree st
( T = r . i & q . i = T . {} )
let i be Element of NAT ; :: thesis: ( i in dom r implies ex T being DecoratedTree st
( T = r . i & q . i = T . {} ) )
assume A8: i in dom r ; :: thesis: ex T being DecoratedTree st
( T = r . i & q . i = T . {} )
then reconsider t = p . i as c-Term of A,V by A7, Th22;
consider vt being finite DecoratedTree such that
A9: vt = r . i and
A10: vt is_an_evaluation_of t,f by A6, A7, A8;
reconsider T = vt as DecoratedTree ;
take T = T; :: thesis: ( T = r . i & q . i = T . {} )
thus T = r . i by A9; :: thesis: q . i = T . {}
thus q . i = t @ f by A2, A7, A8
.= T . {} by A10, Th39 ; :: thesis: verum

end;

then q = roots r by TREES_3:def 18;
hence ((Sym o,(the Sorts of A \/ V)) -tree p) @ f = (((Den o,A) . q) -tree r) . {} by A3, A5, Th39
.= (Den o,A) . q by TREES_4:def 4 ;
:: thesis: verum