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