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) ) )
A1: 1 + (r * r) > 0 + 0 by XREAL_1:10, XREAL_1:65;
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 A2: p = |[(r * (- (p `2 ))),(r * (p `1 ))]| by EUCLID:61;
then p `2 = r * (p `1 ) by EUCLID:56;
then p `1 = - (r * (r * (p `1 ))) by A2, EUCLID:56
.= - ((r * r) * (p `1 )) ;
then (1 + (r * r)) * (p `1 ) = 0 ;
hence A3: p `1 = 0 by A1, XCMPLX_1:6; :: thesis: ( p `2 = 0 & p = 0. (TOP-REAL 2) )
p `1 = r * (- (p `2 )) by A2, EUCLID:56;
then p `2 = - ((r * r) * (p `2 )) by A2, EUCLID:56;
then (1 + (r * r)) * (p `2 ) = 0 ;
hence p `2 = 0 by A1, XCMPLX_1:6; :: thesis: p = 0. (TOP-REAL 2)
hence p = 0. (TOP-REAL 2) by A3, EUCLID:57, EUCLID:58; :: thesis: verum