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 t being c-Term of A,V
for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
t @ f = vt . {}
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 t being c-Term of A,V
for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
t @ f = vt . {}
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
t @ f = vt . {}
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
t @ f = vt . {}
let t be c-Term of A,V; :: thesis: for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
t @ f = vt . {}
let vt be finite DecoratedTree; :: thesis: ( vt is_an_evaluation_of t,f implies t @ f = vt . {} )
assume A1: vt is_an_evaluation_of t,f ; :: thesis: t @ f = vt . {}
consider e being finite DecoratedTree such that
A2: ( e is_an_evaluation_of t,f & t @ f = e . {} ) by Def10;
thus t @ f = vt . {} by A1, A2, Th37; :: thesis: verum