let S be non empty non void ManySortedSign ; 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
t @ f = vt . {}
let A be 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
t @ f = vt . {}
let V be 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 f be 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 t be c-Term of A,V; for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
t @ f = vt . {}
A1:
ex e being finite DecoratedTree st
( e is_an_evaluation_of t,f & t @ f = e . {} )
by Def10;
let vt be finite DecoratedTree; ( vt is_an_evaluation_of t,f implies t @ f = vt . {} )
assume
vt is_an_evaluation_of t,f
; t @ f = vt . {}
hence
t @ f = vt . {}
by A1, Th37; verum