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 )]| by Th3
.= |[(((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 )))]| by Th15 ;
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 ))]| by Th15
.= p1 <X> |[(x * (p2 `1 )),(x * (p2 `2 )),(x * (p2 `3 ))]| by Th3
.= 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