let u, v, w, x be Element of (TOP-REAL 3); :: thesis: ( not u is zero & not x is zero & Dir u = Dir x implies ( |{u,v,w}| = 0 iff |{x,v,w}| = 0 ) )
assume that
A1: not u is zero and
A2: not x is zero and
A3: Dir u = Dir x ; :: thesis: ( |{u,v,w}| = 0 iff |{x,v,w}| = 0 )
A4: are_Prop u,x by A1, A2, A3, ANPROJ_1:22;
then consider a being Real such that
a <> 0 and
A5: u = a * x by ANPROJ_1:1;
consider b being Real such that
b <> 0 and
A6: x = b * u by A4, ANPROJ_1:1;
hereby :: thesis: ( |{x,v,w}| = 0 implies |{u,v,w}| = 0 )
assume A7: |{u,v,w}| = 0 ; :: thesis: |{x,v,w}| = 0
thus |{x,v,w}| = b * |{u,v,w}| by A6, Th26
.= 0 by A7 ; :: thesis: verum
end;
assume A8: |{x,v,w}| = 0 ; :: thesis: |{u,v,w}| = 0
thus |{u,v,w}| = a * |{x,v,w}| by A5, Th26
.= 0 by A8 ; :: thesis: verum