let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of S
for A1 being b₁,S -terms all_vars_including MSAlgebra over S
for s being SortSymbol of S
for x being Element of X . s holds root-tree [x,s] is Element of A1,s
let X be non-empty ManySortedSet of S; :: thesis: for A1 being X,S -terms all_vars_including MSAlgebra over S
for s being SortSymbol of S
for x being Element of X . s holds root-tree [x,s] is Element of A1,s
let A1 be X,S -terms all_vars_including 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 A1,s
let s be SortSymbol of S; :: thesis: for x being Element of X . s holds root-tree [x,s] is Element of A1,s
let x be Element of X . s; :: thesis: root-tree [x,s] is Element of A1,s
FreeGen X is ManySortedSubset of the Sorts of A1 by Def7;
then A1: (FreeGen X) . s c= the Sorts of A1 . 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 A1,s by A1; :: thesis: verum