let p1, p2, q1, q2 be Element of REAL 3; :: thesis: (p1 + p2) <X> (q1 + q2) = (((p1 <X> q1) + (p1 <X> q2)) + (p2 <X> q1)) + (p2 <X> q2)
(p1 + p2) <X> (q1 + q2) = (p1 <X> (q1 + q2)) + (p2 <X> (q1 + q2)) by Th78;
then (p1 + p2) <X> (q1 + q2) = ((p1 <X> q1) + (p1 <X> q2)) + (p2 <X> (q1 + q2)) by Th77;
then (p1 + p2) <X> (q1 + q2) = ((p1 <X> q1) + (p1 <X> q2)) + ((p2 <X> q1) + (p2 <X> q2)) by Th77;
hence (p1 + p2) <X> (q1 + q2) = (((p1 <X> q1) + (p1 <X> q2)) + (p2 <X> q1)) + (p2 <X> q2) by RVSUM_1:15; :: thesis: verum