let P be non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis: for u being non zero Element of (TOP-REAL 3) st P = Dir u holds
u . 2 <> 0
let u be non zero Element of (TOP-REAL 3); :: thesis: ( P = Dir u implies u . 2 <> 0 )
assume A1: P = Dir u ; :: thesis: u . 2 <> 0
consider u9 being non zero Element of (TOP-REAL 3) such that
A2: P = Dir u9 and
A3: u9 . 2 <> 0 by Def3;
are_Prop u,u9 by A1, A2, ANPROJ_1:22;
then consider a being Real such that
A4: a <> 0 and
A5: u = a * u9 by ANPROJ_1:1;
assume u . 2 = 0 ; :: thesis: contradiction
then a * (u9 . 2) = 0 by A5, RVSUM_1:44;
hence contradiction by A3, A4; :: thesis: verum