let u, v be Element of REAL 2; ( ex u being non zero Element of (TOP-REAL 3) st
( P = Dir u & u `3 = 1 & u = |[(u `1),(u `2)]| ) & ex u being non zero Element of (TOP-REAL 3) st
( P = Dir u & u `3 = 1 & v = |[(u `1),(u `2)]| ) implies u = v )
assume that
A6:
ex w being non zero Element of (TOP-REAL 3) st
( P = Dir w & w `3 = 1 & u = |[(w `1),(w `2)]| )
and
A7:
ex w being non zero Element of (TOP-REAL 3) st
( P = Dir w & w `3 = 1 & v = |[(w `1),(w `2)]| )
; u = v
consider w1 being non zero Element of (TOP-REAL 3) such that
A8:
( P = Dir w1 & w1 `3 = 1 & u = |[(w1 `1),(w1 `2)]| )
by A6;
consider w2 being non zero Element of (TOP-REAL 3) such that
A9:
( P = Dir w2 & w2 `3 = 1 & v = |[(w2 `1),(w2 `2)]| )
by A7;
are_Prop w1,w2
by A8, A9, ANPROJ_1:22;
then consider a being Real such that
a <> 0
and
A10:
w1 = a * w2
by ANPROJ_1:1;
1 =
a * (w2 `3)
by A8, A10, EUCLID_5:9
.=
a
by A9
;
then w1 =
|[(1 * (w2 `1)),(1 * (w2 `2)),(1 * (w2 `3))]|
by A10, EUCLID_5:7
.=
w2
by EUCLID_5:3
;
hence
u = v
by A8, A9; verum