theorem :: PCS_0:17

for P, Q being pcs-Str
for p, q being Element of (pcs-sum (P,Q)) holds
( p (--) q iff ( ex p9, q9 being Element of P st
( p9 = p & q9 = q & p9 (--) q9 ) or ex p9, q9 being Element of Q st
( p9 = p & q9 = q & p9 (--) q9 ) ) )