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 s being SortSymbol of S
for x being Element of the Sorts of A . s holds (x -term A,V) @ f = x
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 s being SortSymbol of S
for x being Element of the Sorts of A . s holds (x -term A,V) @ f = x
let V be Variables of A; :: thesis: for f being ManySortedFunction of V,the Sorts of A
for s being SortSymbol of S
for x being Element of the Sorts of A . s holds (x -term A,V) @ f = x
let f be ManySortedFunction of V,the Sorts of A; :: thesis: for s being SortSymbol of S
for x being Element of the Sorts of A . s holds (x -term A,V) @ f = x
let s be SortSymbol of S; :: thesis: for x being Element of the Sorts of A . s holds (x -term A,V) @ f = x
let x be Element of the Sorts of A . s; :: thesis: (x -term A,V) @ f = x
( root-tree x is_an_evaluation_of x -term A,V,f & x = (root-tree x) . {} ) by Th31, TREES_4:3;
hence (x -term A,V) @ f = x by Th39; :: thesis: verum