let u, v, w, x be Element of (TOP-REAL 3); ( 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
; ( |{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;
assume A8:
|{u,v,x}| = 0
; |{u,v,w}| = 0
thus |{u,v,w}| =
a * |{u,v,x}|
by A5, Th28
.=
0
by A8
; verum