set P = pcs-union C;
set TR = the ToleranceRel of (pcs-union C);
set CP = the carrier of (pcs-union C);
set CA = Carrier C;
A1: dom (Carrier C) = I by PARTFUN1:def 4;
A2: the carrier of (pcs-union C) = Union (Carrier C) by Def36;
A3: the ToleranceRel of (pcs-union C) = Union (pcs-ToleranceRels C) by Def36;
A4: dom (pcs-ToleranceRels C) = I by PARTFUN1:def 4;
let x be set ; :: according to RELAT_2:def 1,PCS_0:def 9 :: thesis: ( not x in the carrier of (pcs-union C) or [^,^] in the ToleranceRel of (pcs-union C) )
assume x in the carrier of (pcs-union C) ; :: thesis: [^,^] in the ToleranceRel of (pcs-union C)
then consider P being set such that
A5: x in P and
A6: P in rng (Carrier C) by A2, TARSKI:def 4;
consider i being set such that
A7: i in dom (Carrier C) and
A8: (Carrier C) . i = P by A6, FUNCT_1:def 5;
consider R being 1-sorted such that
A9: R = C . i and
A10: (Carrier C) . i = the carrier of R by A1, A7, PRALG_1:def 13;
reconsider I = I as non empty set by A7, PARTFUN1:def 4;
reconsider i = i as Element of I by A7, PARTFUN1:def 4;
reconsider C = C as pcs-tol-reflexive-yielding () ManySortedSet of ;
A11: (pcs-ToleranceRels C) . i = the ToleranceRel of (C . i) by Def20;
the ToleranceRel of (C . i) is_reflexive_in the carrier of (C . i) by Def9;
then A12: [x,x] in the ToleranceRel of (C . i) by A5, A8, A9, A10, RELAT_2:def 1;
the ToleranceRel of (C . i) in rng (pcs-ToleranceRels C) by A4, A11, FUNCT_1:12;
hence [^,^] in the ToleranceRel of (pcs-union C) by A3, A12, TARSKI:def 4; :: thesis: verum