let x be Real; :: thesis: for p1, p2 being Point of (TOP-REAL 3) holds
( (x * p1) <X> p2 = x * (p1 <X> p2) & (x * p1) <X> p2 = p1 <X> (x * p2) )
let p1, p2 be Point of (TOP-REAL 3); :: thesis: ( (x * p1) <X> p2 = x * (p1 <X> p2) & (x * p1) <X> p2 = p1 <X> (x * p2) )
A1: (x * p1) <X> p2 = |[(x * (p1 `1)),(x * (p1 `2)),(x * (p1 `3))]| <X> p2 by Th7
.= |[(x * (p1 `1)),(x * (p1 `2)),(x * (p1 `3))]| <X> |[(p2 `1),(p2 `2),(p2 `3)]|
.= |[(((x * (p1 `2)) * (p2 `3)) - ((x * (p1 `3)) * (p2 `2))),(((x * (p1 `3)) * (p2 `1)) - ((x * (p1 `1)) * (p2 `3))),(((x * (p1 `1)) * (p2 `2)) - ((x * (p1 `2)) * (p2 `1)))]| ;
then A2: (x * p1) <X> p2 = |[(x * (((p1 `2) * (p2 `3)) - ((p1 `3) * (p2 `2)))),(x * (((p1 `3) * (p2 `1)) - ((p1 `1) * (p2 `3)))),(x * (((p1 `1) * (p2 `2)) - ((p1 `2) * (p2 `1))))]|
.= x * (p1 <X> p2) by Th8 ;
(x * p1) <X> p2 = |[(((p1 `2) * (x * (p2 `3))) - ((p1 `3) * (x * (p2 `2)))),(((p1 `3) * (x * (p2 `1))) - ((p1 `1) * (x * (p2 `3)))),(((p1 `1) * (x * (p2 `2))) - ((p1 `2) * (x * (p2 `1))))]| by A1
.= |[(p1 `1),(p1 `2),(p1 `3)]| <X> |[(x * (p2 `1)),(x * (p2 `2)),(x * (p2 `3))]|
.= p1 <X> |[(x * (p2 `1)),(x * (p2 `2)),(x * (p2 `3))]|
.= p1 <X> (x * p2) by Th7 ;
hence ( (x * p1) <X> p2 = x * (p1 <X> p2) & (x * p1) <X> p2 = p1 <X> (x * p2) ) by A2; :: thesis: verum