let S be non empty non void ManySortedSign ; for X being V5() ManySortedSet of S
for A0 being non-empty b1,S -terms MSAlgebra over S
for t being Element of A0 holds t is Term of S,X
let X be V5() ManySortedSet of S; 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; for t being Element of A0 holds t is Term of S,X
let t be Element of A0; 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; verum