let I be set ; :: thesis:
let C be () ManySortedSet of ; :: thesis:
set R = pcs-union C;
let p, q be Element of (pcs-union C); :: thesis:
A1: dom (pcs-ToleranceRels C) = I by PARTFUN1:def 4;
thus ( p (--) q implies ex i being set ex P being pcs-Str ex p', q' being Element of P st
( i in I & P = C . i & p' = p & q' = q & p' (--) q' ) ) :: thesis:

assume p (--) q ; :: thesis:
then [p,q] in the ToleranceRel of (pcs-union C) by Def7;
then [p,q] in Union (pcs-ToleranceRels C) by Def36;
then consider Z being set such that
A2: [p,q] in Z and
A3: Z in rng (pcs-ToleranceRels C) by TARSKI:def 4;
consider i being set such that
A4: i in dom (pcs-ToleranceRels C) and
A5: (pcs-ToleranceRels C) . i = Z by A3, FUNCT_1:def 5;
reconsider I1 = I as non empty set by A4, PARTFUN1:def 4;
reconsider A1 = C as () ManySortedSet of ;
reconsider i1 = i as Element of I1 by A4, PARTFUN1:def 4;
reconsider P = A1 . i1 as pcs-Str ;
take i ; :: thesis:
take P ; :: thesis:
Z = the ToleranceRel of (A1 . i1) by A5, Def20;
then reconsider p' = p, q' = q as Element of P by A2, ZFMISC_1:106;
take p' ; :: thesis:
take q' ; :: thesis:
thus i in I by A4, PARTFUN1:def 4; :: thesis:
thus ( P = C . i & p' = p & q' = q ) ; :: thesis:
thus [p',q'] in the ToleranceRel of P by A2, A5, Def20; :: according to PCS_0:def 7 :: thesis:

end;

given i being set , P being pcs-Str , p', q' being Element of P such that A6: i in I and
A7: P = C . i and
A8: ( p' = p & q' = q ) and
A9: p' (--) q' ; :: thesis:
A10: [p',q'] in the ToleranceRel of P by A9, Def7;
reconsider I1 = I as non empty set by A6;
reconsider i1 = i as Element of I1 by A6;
reconsider A1 = C as () ManySortedSet of ;
(pcs-ToleranceRels A1) . i1 = the ToleranceRel of (A1 . i1) by Def20;
then the ToleranceRel of (A1 . i1) in rng (pcs-ToleranceRels C) by A1, FUNCT_1:12;
then [p,q] in Union (pcs-ToleranceRels C) by A7, A8, A10, TARSKI:def 4;
hence [p,q] in the ToleranceRel of (pcs-union C) by Def36; :: according to PCS_0:def 7 :: thesis: