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 A1: ( 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 ) ) ; :: thesis: ((Sym o,(the Sorts of A \/ V)) -tree p) @ f = (Den o,A) . q
consider vt being finite DecoratedTree such that
A2: 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
A3: ( len r = len p & vt = ((Den o,A) . (roots r)) -tree r & ( 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 A2, Th35;

now

thus A4: ( dom p = dom p & dom q = dom p & dom r = dom p ) by A1, A3, 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 A5: 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 A4, Th22;
consider vt being finite DecoratedTree such that
A6: ( vt = r . i & vt is_an_evaluation_of t,f ) by A3, A4, A5;
reconsider T = vt as DecoratedTree ;
take T = T; :: thesis: ( T = r . i & q . i = T . {} )
thus T = r . i by A6; :: thesis: q . i = T . {}
thus q . i = t @ f by A1, A4, A5
.= T . {} by A6, 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 A2, A3, Th39
.= (Den o,A) . q by TREES_4:def 4 ;
:: thesis: verum