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 Th128
.= - ((p3 <X> p1) + (p3 <X> p2)) by Th137
.= - ((p3 <X> p1) - (p2 <X> p3)) by Th128
.= (- (p3 <X> p1)) + (p2 <X> p3) by RVSUM_1:57 ;
hence (p1 + p2) <X> p3 = (p1 <X> p3) + (p2 <X> p3) by Th128; :: thesis: verum