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 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 over 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
x = (root-tree x) . {} by TREES_4:3;
hence (x -term (A,V)) @ f = x by Th31, Th39; :: thesis: verum