let x be set ; :: thesis: for S being non void Signature
for X being V5() 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 V5() ManySortedSet of the carrier of S holds
( x is Element of (FreeMSA X) iff x is Term of S,X )
let X be V5() 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:12
.= Union (FreeSort X) by CARD_3:def 4 ;
FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #) by MSAFREE:def 16;
hence ( x is Element of (FreeMSA X) iff x is Term of S,X ) by A1; :: thesis: verum