let x be set ; :: thesis: for S being non void Signature

for X being V8() 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 V8() ManySortedSet of the carrier of S holds

( x is Element of (FreeMSA X) iff x is Term of S,X )

let X be V8() 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

for X being V8() 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 V8() ManySortedSet of the carrier of S holds

( x is Element of (FreeMSA X) iff x is Term of S,X )

let X be V8() 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