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

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

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

end;

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