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 2;
A2:
dom (pcs-InternalRels (MSSet (P,Q))) = {0,1}
by PARTFUN1:def 2;
A3:
dom (pcs-ToleranceRels (MSSet (P,Q))) = {0,1}
by PARTFUN1:def 2;
A4:
(MSSet (P,Q)) . 0 = P
by FUNCT_4:63;
A5:
(MSSet (P,Q)) . 1 = Q
by FUNCT_4:63;
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:3;
the
carrier of
Q in rng (Carrier (MSSet (P,Q)))
by A1, A5, A9, FUNCT_1:3;
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 3;
(
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:3;
the
InternalRel of
Q in rng (pcs-InternalRels (MSSet (P,Q)))
by A2, A5, A18, FUNCT_1:3;
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 3;
(
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:3;
the
ToleranceRel of
Q in rng (pcs-ToleranceRels (MSSet (P,Q)))
by A3, A5, A26, FUNCT_1:3;
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 3;
(
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