let r be Real; 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; ( (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; verum