let x be set ; 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; 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; 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; ( [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 ( x in X . s implies [x,s] in the carrier of (DTConMSA X) )
assume
[x,s] in the
carrier of
(DTConMSA X)
;
x in X . sthen
[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;
verum
end;
assume
x in X . s
; [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; verum