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