let u, v be non zero Element of (TOP-REAL 3); :: thesis: for k being non zero Real st u = k * v holds
Dir u = Dir v
let k be non zero Real; :: thesis: ( u = k * v implies Dir u = Dir v )
assume u = k * v ; :: thesis: Dir u = Dir v
then are_Prop u,v by ANPROJ_1:1;
hence Dir u = Dir v by ANPROJ_1:22; :: thesis: verum