let u, v be non zero Element of (TOP-REAL 3); ( Dir u = Dir v & u . 3 = v . 3 & v . 3 <> 0 implies u = v )
assume that
A1:
Dir u = Dir v
and
A2:
u . 3 = v . 3
and
A3:
v . 3 <> 0
; u = v
are_Prop u,v
by A1, ANPROJ_1:22;
then consider a being Real such that
a <> 0
and
A4:
u = a * v
by ANPROJ_1:1;
reconsider b = 1 - a, c = v . 3 as Real ;
A5: |[(u `1),(u `2),(u `3)]| =
a * v
by A4, EUCLID_5:3
.=
|[(a * (v `1)),(a * (v `2)),(a * (v `3))]|
by EUCLID_5:7
;
v . 3 =
u `3
by A2, EUCLID_5:def 3
.=
a * (v `3)
by A5, FINSEQ_1:78
.=
a * (v . 3)
by EUCLID_5:def 3
;
then
( (1 - a) * (v . 3) = 0 & c = v . 3 )
;
then
b = 0
by A3;
then u =
|[(1 * (v `1)),(1 * (v `2)),(1 * (v `3))]|
by A4, EUCLID_5:7
.=
v
by EUCLID_5:3
;
hence
u = v
; verum