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: ( (p1 <X> p2) . 1 = ((p1 . 2) * (p2 . 3)) - ((p1 . 3) * (p2 . 2)) & (p1 <X> p2) . 2 = ((p1 . 3) * (p2 . 1)) - ((p1 . 1) * (p2 . 3)) & (p1 <X> p2) . 3 = ((p1 . 1) * (p2 . 2)) - ((p1 . 2) * (p2 . 1)) ) by FINSEQ_1:45;
A2: (r * p1) <X> p2 = |[(r * (p1 . 1)),(r * (p1 . 2)),(r * (p1 . 3))]| <X> p2 by Lm1
.= |[(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 Lm13 ;
then A3: (r * p1) <X> p2 = |[(r * ((p1 <X> p2) . 1)),(r * ((p1 <X> p2) . 2)),(r * ((p1 <X> p2) . 3))]| by A1
.= r * (p1 <X> p2) by Lm1 ;
(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 A2
.= |[(p1 . 1),(p1 . 2),(p1 . 3)]| <X> |[(r * (p2 . 1)),(r * (p2 . 2)),(r * (p2 . 3))]| by Lm13
.= p1 <X> |[(r * (p2 . 1)),(r * (p2 . 2)),(r * (p2 . 3))]| by Th1
.= p1 <X> (r * p2) by Lm1 ;
hence ( (r * p1) <X> p2 = r * (p1 <X> p2) & (r * p1) <X> p2 = p1 <X> (r * p2) ) by A3; :: thesis: verum