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 () 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 () 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 () iff x in X . s )

let s be SortSymbol of S; :: thesis: ( [x,s] in the carrier of () iff x in X . s )
A1: DTConMSA X = DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union ())),(REL X) #) by MSAFREE:def 8;
A2: dom () = 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 () )
assume [x,s] in the carrier of () ; :: thesis: x in X . s
then [x,s] in Union () by ;
then consider y being object such that
A4: y in dom () and
A5: [x,s] in () . y by CARD_5:2;
(coprod X) . y = coprod (y,X) by ;
then consider z being set such that
A6: z in X . y and
A7: [x,s] = [z,y] by ;
x = z by ;
hence x in X . s by ; :: thesis: verum
end;
assume x in X . s ; :: thesis: [x,s] in the carrier of ()
then [x,s] in coprod (s,X) by MSAFREE:def 2;
then [x,s] in () . s by MSAFREE:def 3;
then [x,s] in Union () by ;
hence [x,s] in the carrier of () by ; :: thesis: verum