let u, v be Element of REAL 2; :: thesis: ( 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)]| ) ; :: thesis: 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; :: thesis: verum