let S be non empty non void ManySortedSign ; :: thesis: for X being V5() ManySortedSet of S
for A being b₁,S -terms MSAlgebra over S
for s being SortSymbol of S
for x being Element of X . s holds root-tree [x,s] is Element of A,s
let X be V5() ManySortedSet of S; :: thesis: for A being X,S -terms MSAlgebra over S
for s being SortSymbol of S
for x being Element of X . s holds root-tree [x,s] is Element of A,s
let A be X,S -terms MSAlgebra over S; :: thesis: for s being SortSymbol of S
for x being Element of X . s holds root-tree [x,s] is Element of A,s
let s be SortSymbol of S; :: thesis: for x being Element of X . s holds root-tree [x,s] is Element of A,s
let x be Element of X . s; :: thesis: root-tree [x,s] is Element of A,s
FreeGen X is ManySortedSubset of the Sorts of A by Def6;
then A1: (FreeGen X) . s c= the Sorts of A . s by PBOOLE:def 2, PBOOLE:def 18;
root-tree [x,s] in FreeGen (s,X) by MSAFREE:def 15;
then root-tree [x,s] in (FreeGen X) . s by MSAFREE:def 16;
hence root-tree [x,s] is Element of A,s by A1; :: thesis: verum