theorem :: EUCLID_8:88

for p1, p2, q1, q2 being Element of REAL 3 holds (p1 + p2) <X> (q1 + q2) = (((p1 <X> q1) + (p1 <X> q2)) + (p2 <X> q1)) + (p2 <X> q2)