let x be set ; :: thesis: for S being non void Signature
for X being ManySortedSet of the carrier of S
for s being SortSymbol of S holds
( [x,s] in the carrier of (DTConMSA X) iff x in X . s )
let S be non void Signature; :: thesis: for X being ManySortedSet of the carrier of S
for s being SortSymbol of S holds
( [x,s] in the carrier of (DTConMSA X) iff x in X . s )
let X be ManySortedSet of the carrier of S; :: thesis: for s being SortSymbol of S holds
( [x,s] in the carrier of (DTConMSA X) iff x in X . s )
let s be SortSymbol of S; :: thesis: ( [x,s] in the carrier of (DTConMSA X) iff x in X . s )
A1: DTConMSA X = DTConstrStr(# ([:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X))),(REL X) #) by MSAFREE:def 10;
s in the carrier of S ;
then s <> the carrier of S ;
then not s in {the carrier of S} by TARSKI:def 1;
then A2: not [x,s] in [:the carrier' of S,{the carrier of S}:] by ZFMISC_1:106;
A3: dom (coprod X) = the carrier of S by PBOOLE:def 3;

hereby :: thesis: ( x in X . s implies [x,s] in the carrier of (DTConMSA X) )

assume [x,s] in the carrier of (DTConMSA X) ; :: thesis: x in X . s
then [x,s] in Union (coprod X) by A1, A2, XBOOLE_0:def 3;
then consider y being set such that
A4: ( y in dom (coprod X) & [x,s] in (coprod X) . y ) by CARD_5:10;
(coprod X) . y = coprod y,X by A3, A4, MSAFREE:def 3;
then consider z being set such that
A5: ( z in X . y & [x,s] = [z,y] ) by A3, A4, MSAFREE:def 2;
( x = z & s = y ) by A5, ZFMISC_1:33;
hence x in X . s by A5; :: thesis: verum

end;

assume x in X . s ; :: thesis: [x,s] in the carrier of (DTConMSA X)
then [x,s] in coprod s,X by MSAFREE:def 2;
then [x,s] in (coprod X) . s by MSAFREE:def 3;
then [x,s] in Union (coprod X) by A3, CARD_5:10;
hence [x,s] in the carrier of (DTConMSA X) by A1, XBOOLE_0:def 3; :: thesis: verum