let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of S
for A0 being non-empty b₁,S -terms MSAlgebra over S
for t being Element of A0 holds t is Term of S,X
let X be non-empty ManySortedSet of S; :: thesis: for A0 being non-empty X,S -terms MSAlgebra over S
for t being Element of A0 holds t is Term of S,X
let A0 be non-empty X,S -terms MSAlgebra over S; :: thesis: for t being Element of A0 holds t is Term of S,X
let t be Element of A0; :: thesis: t is Term of S,X
consider s being object such that
A1: ( s in dom the Sorts of A0 & t in the Sorts of A0 . s ) by CARD_5:2;
reconsider s = s as SortSymbol of S by A1;
the Sorts of A0 is ManySortedSubset of the Sorts of (Free (S,X)) by Def6;
then the Sorts of A0 . s c= the Sorts of (Free (S,X)) . s by PBOOLE:def 2, PBOOLE:def 18;
then t is Element of the Sorts of (Free (S,X)) . s by A1;
then t is Element of (FreeMSA X) by MSAFREE3:31;
hence t is Term of S,X by MSAFREE3:6; :: thesis: verum