let P, Q be pcs-Str ; ( 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
by FUNCT_4:66;
A5:
(MSSet P,Q) . 1 = Q
by FUNCT_4:66;
A6:
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))
XBOOLE_0:def 10 Union (Carrier (MSSet P,Q)) c= the carrier of H1(P,Q)proof
let x be
set ;
TARSKI:def 3 ( 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)
;
x in Union (Carrier (MSSet P,Q))
then A7:
(
x in the
carrier of
P or
x in the
carrier of
Q )
by XBOOLE_0:def 3;
A8:
(Carrier (MSSet P,Q)) . z = the
carrier of
((MSSet P,Q) . z)
by Def1;
A9:
(Carrier (MSSet P,Q)) . j = the
carrier of
((MSSet P,Q) . j)
by Def1;
A10:
the
carrier of
P in rng (Carrier (MSSet P,Q))
by A1, A4, A8, FUNCT_1:12;
the
carrier of
Q in rng (Carrier (MSSet P,Q))
by A1, A5, A9, FUNCT_1:12;
hence
x in Union (Carrier (MSSet P,Q))
by A7, A10, TARSKI:def 4;
verum
end;
let x be
set ;
TARSKI:def 3 ( 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))
;
x in the carrier of H1(P,Q)
then consider Z being
set such that A11:
x in Z
and A12:
Z in rng (Carrier (MSSet P,Q))
by TARSKI:def 4;
consider i being
set such that A13:
i in dom (Carrier (MSSet P,Q))
and A14:
(Carrier (MSSet P,Q)) . i = Z
by A12, FUNCT_1:def 5;
(
i = 0 or
i = 1 )
by A1, A13, TARSKI:def 2;
then
(
Z = the
carrier of
((MSSet P,Q) . z) or
Z = the
carrier of
((MSSet P,Q) . j) )
by A14, Def1;
hence
x in the
carrier of
H1(
P,
Q)
by A4, A5, A11, XBOOLE_0:def 3;
verum
end;
A15:
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))
XBOOLE_0:def 10 Union (pcs-InternalRels (MSSet P,Q)) c= the InternalRel of H1(P,Q)proof
let x be
set ;
TARSKI:def 3 ( 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)
;
x in Union (pcs-InternalRels (MSSet P,Q))
then A16:
(
x in the
InternalRel of
P or
x in the
InternalRel of
Q )
by XBOOLE_0:def 3;
A17:
(pcs-InternalRels (MSSet P,Q)) . z = the
InternalRel of
((MSSet P,Q) . z)
by Def6;
A18:
(pcs-InternalRels (MSSet P,Q)) . j = the
InternalRel of
((MSSet P,Q) . j)
by Def6;
A19:
the
InternalRel of
P in rng (pcs-InternalRels (MSSet P,Q))
by A2, A4, A17, FUNCT_1:12;
the
InternalRel of
Q in rng (pcs-InternalRels (MSSet P,Q))
by A2, A5, A18, FUNCT_1:12;
hence
x in Union (pcs-InternalRels (MSSet P,Q))
by A16, A19, TARSKI:def 4;
verum
end;
let x be
set ;
TARSKI:def 3 ( 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))
;
x in the InternalRel of H1(P,Q)
then consider Z being
set such that A20:
x in Z
and A21:
Z in rng (pcs-InternalRels (MSSet P,Q))
by TARSKI:def 4;
consider i being
set such that A22:
i in dom (pcs-InternalRels (MSSet P,Q))
and A23:
(pcs-InternalRels (MSSet P,Q)) . i = Z
by A21, FUNCT_1:def 5;
(
i = 0 or
i = 1 )
by A2, A22, TARSKI:def 2;
then
(
Z = the
InternalRel of
((MSSet P,Q) . z) or
Z = the
InternalRel of
((MSSet P,Q) . j) )
by A23, Def6;
hence
x in the
InternalRel of
H1(
P,
Q)
by A4, A5, A20, XBOOLE_0:def 3;
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))
XBOOLE_0:def 10 Union (pcs-ToleranceRels (MSSet P,Q)) c= the ToleranceRel of H1(P,Q)proof
let x be
set ;
TARSKI:def 3 ( 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)
;
x in Union (pcs-ToleranceRels (MSSet P,Q))
then A24:
(
x in the
ToleranceRel of
P or
x in the
ToleranceRel of
Q )
by XBOOLE_0:def 3;
A25:
(pcs-ToleranceRels (MSSet P,Q)) . z = the
ToleranceRel of
((MSSet P,Q) . z)
by Def20;
A26:
(pcs-ToleranceRels (MSSet P,Q)) . j = the
ToleranceRel of
((MSSet P,Q) . j)
by Def20;
A27:
the
ToleranceRel of
P in rng (pcs-ToleranceRels (MSSet P,Q))
by A3, A4, A25, FUNCT_1:12;
the
ToleranceRel of
Q in rng (pcs-ToleranceRels (MSSet P,Q))
by A3, A5, A26, FUNCT_1:12;
hence
x in Union (pcs-ToleranceRels (MSSet P,Q))
by A24, A27, TARSKI:def 4;
verum
end;
let x be
set ;
TARSKI:def 3 ( 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))
;
x in the ToleranceRel of H1(P,Q)
then consider Z being
set such that A28:
x in Z
and A29:
Z in rng (pcs-ToleranceRels (MSSet P,Q))
by TARSKI:def 4;
consider i being
set such that A30:
i in dom (pcs-ToleranceRels (MSSet P,Q))
and A31:
(pcs-ToleranceRels (MSSet P,Q)) . i = Z
by A29, FUNCT_1:def 5;
(
i = 0 or
i = 1 )
by A3, A30, TARSKI:def 2;
then
(
Z = the
ToleranceRel of
((MSSet P,Q) . z) or
Z = the
ToleranceRel of
((MSSet P,Q) . j) )
by A31, Def20;
hence
x in the
ToleranceRel of
H1(
P,
Q)
by A4, A5, A28, XBOOLE_0:def 3;
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 A6, A15, Def36; verum