let p1, p2, p3 be Point of (TOP-REAL 3); :: thesis: (p1 + p2) <X> p3 = (p1 <X> p3) + (p2 <X> p3)
(p1 + p2) <X> p3 = - (p3 <X> (p1 + p2)) by Th17
.= - ((p3 <X> p1) + (p3 <X> p2)) by Th23
.= - ((p3 <X> p1) - (p2 <X> p3)) by Th17
.= (- (p3 <X> p1)) + (p2 <X> p3) by RLVECT_1:33 ;
hence (p1 + p2) <X> p3 = (p1 <X> p3) + (p2 <X> p3) by Th17; :: thesis: verum