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

hereby :: thesis: ( |{u,x,w}| = 0 implies |{u,v,w}| = 0 )

assume A7: |{u,v,w}| = 0 ; :: thesis: |{u,x,w}| = 0
thus |{u,x,w}| = b * |{u,v,w}| by A6, Th27
.= 0 by A7 ; :: thesis: verum

end;

assume A8: |{u,x,w}| = 0 ; :: thesis: |{u,v,w}| = 0
thus |{u,v,w}| = a * |{u,x,w}| by A5, Th27
.= 0 by A8 ; :: thesis: verum