let P, Q be pcs-Str ; :: thesis: ( the carrier of (pcs-sum P,Q) = the carrier of P \/ the carrier of Q & the InternalRel of (pcs-sum P,Q) = the InternalRel of P \/ the InternalRel of Q & the ToleranceRel of (pcs-sum P,Q) = the ToleranceRel of P \/ the ToleranceRel of Q )
set S = H1(P,Q);
set f = MSSet P,Q;
A1:
dom (Carrier (MSSet P,Q)) = {0 ,1}
by PARTFUN1:def 4;
A2:
dom (pcs-InternalRels (MSSet P,Q)) = {0 ,1}
by PARTFUN1:def 4;
A3:
dom (pcs-ToleranceRels (MSSet P,Q)) = {0 ,1}
by PARTFUN1:def 4;
A4:
( (MSSet P,Q) . 0 = P & (MSSet P,Q) . 1 = Q )
by FUNCT_4:66;
A5:
the carrier of H1(P,Q) = Union (Carrier (MSSet P,Q))
proof
thus
the
carrier of
H1(
P,
Q)
c= Union (Carrier (MSSet P,Q))
:: according to XBOOLE_0:def 10 :: thesis: Union (Carrier (MSSet P,Q)) c= the carrier of H1(P,Q)proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in the carrier of H1(P,Q) or x in Union (Carrier (MSSet P,Q)) )
assume
x in the
carrier of
H1(
P,
Q)
;
:: thesis: x in Union (Carrier (MSSet P,Q))
then A6:
(
x in the
carrier of
P or
x in the
carrier of
Q )
by XBOOLE_0:def 3;
(
(Carrier (MSSet P,Q)) . z = the
carrier of
((MSSet P,Q) . z) &
(Carrier (MSSet P,Q)) . j = the
carrier of
((MSSet P,Q) . j) )
by Def1;
then
( the
carrier of
P in rng (Carrier (MSSet P,Q)) & the
carrier of
Q in rng (Carrier (MSSet P,Q)) )
by A1, A4, FUNCT_1:12;
hence
x in Union (Carrier (MSSet P,Q))
by A6, TARSKI:def 4;
:: thesis: verum
end;
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in Union (Carrier (MSSet P,Q)) or x in the carrier of H1(P,Q) )
assume
x in Union (Carrier (MSSet P,Q))
;
:: thesis: x in the carrier of H1(P,Q)
then consider Z being
set such that A7:
x in Z
and A8:
Z in rng (Carrier (MSSet P,Q))
by TARSKI:def 4;
consider i being
set such that A9:
i in dom (Carrier (MSSet P,Q))
and A10:
(Carrier (MSSet P,Q)) . i = Z
by A8, FUNCT_1:def 5;
(
i = 0 or
i = 1 )
by A1, A9, TARSKI:def 2;
then
(
Z = the
carrier of
((MSSet P,Q) . z) or
Z = the
carrier of
((MSSet P,Q) . j) )
by A10, Def1;
hence
x in the
carrier of
H1(
P,
Q)
by A4, A7, XBOOLE_0:def 3;
:: thesis: verum
end;
A11:
the InternalRel of H1(P,Q) = Union (pcs-InternalRels (MSSet P,Q))
proof
thus
the
InternalRel of
H1(
P,
Q)
c= Union (pcs-InternalRels (MSSet P,Q))
:: according to XBOOLE_0:def 10 :: thesis: Union (pcs-InternalRels (MSSet P,Q)) c= the InternalRel of H1(P,Q)proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in the InternalRel of H1(P,Q) or x in Union (pcs-InternalRels (MSSet P,Q)) )
assume
x in the
InternalRel of
H1(
P,
Q)
;
:: thesis: x in Union (pcs-InternalRels (MSSet P,Q))
then A12:
(
x in the
InternalRel of
P or
x in the
InternalRel of
Q )
by XBOOLE_0:def 3;
(
(pcs-InternalRels (MSSet P,Q)) . z = the
InternalRel of
((MSSet P,Q) . z) &
(pcs-InternalRels (MSSet P,Q)) . j = the
InternalRel of
((MSSet P,Q) . j) )
by Def6;
then
( the
InternalRel of
P in rng (pcs-InternalRels (MSSet P,Q)) & the
InternalRel of
Q in rng (pcs-InternalRels (MSSet P,Q)) )
by A2, A4, FUNCT_1:12;
hence
x in Union (pcs-InternalRels (MSSet P,Q))
by A12, TARSKI:def 4;
:: thesis: verum
end;
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in Union (pcs-InternalRels (MSSet P,Q)) or x in the InternalRel of H1(P,Q) )
assume
x in Union (pcs-InternalRels (MSSet P,Q))
;
:: thesis: x in the InternalRel of H1(P,Q)
then consider Z being
set such that A13:
x in Z
and A14:
Z in rng (pcs-InternalRels (MSSet P,Q))
by TARSKI:def 4;
consider i being
set such that A15:
i in dom (pcs-InternalRels (MSSet P,Q))
and A16:
(pcs-InternalRels (MSSet P,Q)) . i = Z
by A14, FUNCT_1:def 5;
(
i = 0 or
i = 1 )
by A2, A15, TARSKI:def 2;
then
(
Z = the
InternalRel of
((MSSet P,Q) . z) or
Z = the
InternalRel of
((MSSet P,Q) . j) )
by A16, Def6;
hence
x in the
InternalRel of
H1(
P,
Q)
by A4, A13, XBOOLE_0:def 3;
:: thesis: verum
end;
the ToleranceRel of H1(P,Q) = Union (pcs-ToleranceRels (MSSet P,Q))
proof
thus
the
ToleranceRel of
H1(
P,
Q)
c= Union (pcs-ToleranceRels (MSSet P,Q))
:: according to XBOOLE_0:def 10 :: thesis: Union (pcs-ToleranceRels (MSSet P,Q)) c= the ToleranceRel of H1(P,Q)proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in the ToleranceRel of H1(P,Q) or x in Union (pcs-ToleranceRels (MSSet P,Q)) )
assume
x in the
ToleranceRel of
H1(
P,
Q)
;
:: thesis: x in Union (pcs-ToleranceRels (MSSet P,Q))
then A17:
(
x in the
ToleranceRel of
P or
x in the
ToleranceRel of
Q )
by XBOOLE_0:def 3;
(
(pcs-ToleranceRels (MSSet P,Q)) . z = the
ToleranceRel of
((MSSet P,Q) . z) &
(pcs-ToleranceRels (MSSet P,Q)) . j = the
ToleranceRel of
((MSSet P,Q) . j) )
by Def20;
then
( the
ToleranceRel of
P in rng (pcs-ToleranceRels (MSSet P,Q)) & the
ToleranceRel of
Q in rng (pcs-ToleranceRels (MSSet P,Q)) )
by A3, A4, FUNCT_1:12;
hence
x in Union (pcs-ToleranceRels (MSSet P,Q))
by A17, TARSKI:def 4;
:: thesis: verum
end;
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in Union (pcs-ToleranceRels (MSSet P,Q)) or x in the ToleranceRel of H1(P,Q) )
assume
x in Union (pcs-ToleranceRels (MSSet P,Q))
;
:: thesis: x in the ToleranceRel of H1(P,Q)
then consider Z being
set such that A18:
x in Z
and A19:
Z in rng (pcs-ToleranceRels (MSSet P,Q))
by TARSKI:def 4;
consider i being
set such that A20:
i in dom (pcs-ToleranceRels (MSSet P,Q))
and A21:
(pcs-ToleranceRels (MSSet P,Q)) . i = Z
by A19, FUNCT_1:def 5;
(
i = 0 or
i = 1 )
by A3, A20, TARSKI:def 2;
then
(
Z = the
ToleranceRel of
((MSSet P,Q) . z) or
Z = the
ToleranceRel of
((MSSet P,Q) . j) )
by A21, Def20;
hence
x in the
ToleranceRel of
H1(
P,
Q)
by A4, A18, XBOOLE_0:def 3;
:: thesis: verum
end;
hence
( the carrier of (pcs-sum P,Q) = the carrier of P \/ the carrier of Q & the InternalRel of (pcs-sum P,Q) = the InternalRel of P \/ the InternalRel of Q & the ToleranceRel of (pcs-sum P,Q) = the ToleranceRel of P \/ the ToleranceRel of Q )
by A5, A11, Def36; :: thesis: verum