let P, Q be pcs-Str ; pcs-sum (P,Q) = pcs-Str(# ( the carrier of P \/ the carrier of Q),( the InternalRel of P \/ the InternalRel of Q),( the ToleranceRel of P \/ the ToleranceRel of Q) #)
A1:
the carrier of (pcs-sum (P,Q)) = the carrier of P \/ the carrier of Q
by Th14;
the InternalRel of (pcs-sum (P,Q)) = the InternalRel of P \/ the InternalRel of Q
by Th14;
hence
pcs-sum (P,Q) = pcs-Str(# ( the carrier of P \/ the carrier of Q),( the InternalRel of P \/ the InternalRel of Q),( the ToleranceRel of P \/ the ToleranceRel of Q) #)
by A1, Th14; verum