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 8;
A2: dom (coprod X) = the carrier of S by PARTFUN1:def 2;
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 A3: not [x,s] in [: the carrier' of S,{ the carrier of S}:] by ZFMISC_1:87;

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, A3, XBOOLE_0:def 3;
then consider y being object such that
A4: y in dom (coprod X) and
A5: [x,s] in (coprod X) . y by CARD_5:2;
(coprod X) . y = coprod (y,X) by A4, MSAFREE:def 3;
then consider z being set such that
A6: z in X . y and
A7: [x,s] = [z,y] by A4, A5, MSAFREE:def 2;
x = z by A7, XTUPLE_0:1;
hence x in X . s by A6, A7, XTUPLE_0:1; :: 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 A2, CARD_5:2;
hence [x,s] in the carrier of (DTConMSA X) by A1, XBOOLE_0:def 3; :: thesis: verum