let r be Real; :: thesis: for p1, p2 being Element of REAL 3 holds
( (r * p1) <X> p2 = r * (p1 <X> p2) & (r * p1) <X> p2 = p1 <X> (r * p2) )
let p1, p2 be Element of REAL 3; :: thesis: ( (r * p1) <X> p2 = r * (p1 <X> p2) & (r * p1) <X> p2 = p1 <X> (r * p2) )
A1: (r * p1) <X> p2 = |[(r * (p1 . 1)),(r * (p1 . 2)),(r * (p1 . 3))]| <X> p2 by Th49
.= |[(r * (p1 . 1)),(r * (p1 . 2)),(r * (p1 . 3))]| <X> |[(p2 . 1),(p2 . 2),(p2 . 3)]| by Th1
.= |[(((r * (p1 . 2)) * (p2 . 3)) - ((r * (p1 . 3)) * (p2 . 2))),(((r * (p1 . 3)) * (p2 . 1)) - ((r * (p1 . 1)) * (p2 . 3))),(((r * (p1 . 1)) * (p2 . 2)) - ((r * (p1 . 2)) * (p2 . 1)))]| by Th75 ;
then A2: (r * p1) <X> p2 = |[(r * (((p1 . 2) * (p2 . 3)) - ((p1 . 3) * (p2 . 2)))),(r * (((p1 . 3) * (p2 . 1)) - ((p1 . 1) * (p2 . 3)))),(r * (((p1 . 1) * (p2 . 2)) - ((p1 . 2) * (p2 . 1))))]|
.= r * (p1 <X> p2) by Th50 ;
(r * p1) <X> p2 = |[(((p1 . 2) * (r * (p2 . 3))) - ((p1 . 3) * (r * (p2 . 2)))),(((p1 . 3) * (r * (p2 . 1))) - ((p1 . 1) * (r * (p2 . 3)))),(((p1 . 1) * (r * (p2 . 2))) - ((p1 . 2) * (r * (p2 . 1))))]| by A1
.= |[(p1 . 1),(p1 . 2),(p1 . 3)]| <X> |[(r * (p2 . 1)),(r * (p2 . 2)),(r * (p2 . 3))]| by Th75
.= p1 <X> |[(r * (p2 . 1)),(r * (p2 . 2)),(r * (p2 . 3))]| by Th1
.= p1 <X> (r * p2) by Th49 ;
hence ( (r * p1) <X> p2 = r * (p1 <X> p2) & (r * p1) <X> p2 = p1 <X> (r * p2) ) by A2; :: thesis: verum