let p1, p2, p3 be Element of REAL 3; :: thesis: (p1 + p2) <X> p3 = (p1 <X> p3) + (p2 <X> p3)
(p1 + p2) <X> p3 = - (p3 <X> (p1 + p2)) by Th74
.= - ((p3 <X> p1) + (p3 <X> p2)) by Th77
.= - ((p3 <X> p1) - (p2 <X> p3)) by Th74
.= (- (p3 <X> p1)) + (p2 <X> p3) by RVSUM_1:36 ;
hence (p1 + p2) <X> p3 = (p1 <X> p3) + (p2 <X> p3) by Th74; :: thesis: verum