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