let x be set ; :: thesis: for S being non void Signature
for X being non-empty ManySortedSet of the carrier of S holds
( x is Element of (FreeMSA X) iff x is Term of S,X )
let S be non void Signature; :: thesis: for X being non-empty ManySortedSet of the carrier of S holds
( x is Element of (FreeMSA X) iff x is Term of S,X )
let X be non-empty ManySortedSet of the carrier of S; :: thesis: ( x is Element of (FreeMSA X) iff x is Term of S,X )
A1: S -Terms X = TS (DTConMSA X) by MSATERM:def 1
.= union (rng (FreeSort X)) by MSAFREE:11
.= Union (FreeSort X) by CARD_3:def 4 ;
FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #) by MSAFREE:def 14;
hence ( x is Element of (FreeMSA X) iff x is Term of S,X ) by A1; :: thesis: verum