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;

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

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 in X . s
; :: thesis: [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;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

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