let P, Q be pcs-Str ; :: thesis: 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; :: thesis: verum