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