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) #)
( the carrier of (pcs-sum P,Q) = the carrier of P \/ the carrier of Q & the InternalRel of (pcs-sum P,Q) = the InternalRel of P \/ the InternalRel of Q & the ToleranceRel of (pcs-sum P,Q) = the ToleranceRel of P \/ the ToleranceRel 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) #) ; :: thesis: verum