let p, q be Point of (TOP-REAL 2); :: thesis: for r being Real st p `1 = q `2 & - (p `2 ) = q `1 & p = r * q holds
( p `1 = 0 & p `2 = 0 & p = 0. (TOP-REAL 2) )
let r be Real; :: thesis: ( p `1 = q `2 & - (p `2 ) = q `1 & p = r * q implies ( p `1 = 0 & p `2 = 0 & p = 0. (TOP-REAL 2) ) )
assume ( p `1 = q `2 & - (p `2 ) = q `1 & p = r * q ) ; :: thesis: ( p `1 = 0 & p `2 = 0 & p = 0. (TOP-REAL 2) )
then p = |[(r * (- (p `2 ))),(r * (p `1 ))]| by EUCLID:61;
then A1: ( p `1 = r * (- (p `2 )) & p `2 = r * (p `1 ) ) by EUCLID:56;
then p `1 = - (r * (r * (p `1 ))) by XCMPLX_1:175
.= - ((r * r) * (p `1 )) ;
then A2: (1 + (r * r)) * (p `1 ) = 0 ;
A3: 1 + (r * r) > 0 + 0 by XREAL_1:10, XREAL_1:65;
hence A4: p `1 = 0 by A2, XCMPLX_1:6; :: thesis: ( p `2 = 0 & p = 0. (TOP-REAL 2) )
p `2 = - ((r * r) * (p `2 )) by A1;
then (1 + (r * r)) * (p `2 ) = 0 ;
hence p `2 = 0 by A3, XCMPLX_1:6; :: thesis: p = 0. (TOP-REAL 2)
hence p = 0. (TOP-REAL 2) by A4, EUCLID:57, EUCLID:58; :: thesis: verum