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 t being c-Term of A,V
for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
for p being Node of t holds vt . p = (t | 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 t being c-Term of A,V
for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
for p being Node of t holds vt . p = (t | p) @ f
let V be Variables of A; :: thesis: for f being ManySortedFunction of V, the Sorts of A
for t being c-Term of A,V
for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
for p being Node of t holds vt . p = (t | p) @ f
let f be ManySortedFunction of V, the Sorts of A; :: thesis: for t being c-Term of A,V
for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
for p being Node of t holds vt . p = (t | p) @ f
let t be c-Term of A,V; :: thesis: for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
for p being Node of t holds vt . p = (t | p) @ f
let vt be finite DecoratedTree; :: thesis: ( vt is_an_evaluation_of t,f implies for p being Node of t holds vt . p = (t | p) @ f )
assume A1: vt is_an_evaluation_of t,f ; :: thesis: for p being Node of t holds vt . p = (t | p) @ f
let p be Node of t; :: thesis: vt . p = (t | p) @ f
reconsider n = p as Node of vt by A1;
A2: n ^ {} = n by FINSEQ_1:34;
A3: {} in (dom vt) | p by TREES_1:22;
(t | p) @ f = (vt | n) . (<*> NAT) by A1, Th34, Th39;
hence vt . p = (t | p) @ f by A2, A3, TREES_2:def 10; :: thesis: verum