let u1, u2 be Element of circle (0,0,1); :: thesis: ( ex u being non zero Element of (TOP-REAL 3) st
( P = Dir u & u . 3 = 1 & u1 = |[(u . 1),(u . 2)]| ) & ex u being non zero Element of (TOP-REAL 3) st
( P = Dir u & u . 3 = 1 & u2 = |[(u . 1),(u . 2)]| ) implies u1 = u2 )
assume that
A6: ex u being non zero Element of (TOP-REAL 3) st
( P = Dir u & u . 3 = 1 & u1 = |[(u . 1),(u . 2)]| ) and
A7: ex v being non zero Element of (TOP-REAL 3) st
( P = Dir v & v . 3 = 1 & u2 = |[(v . 1),(v . 2)]| ) ; :: thesis: u1 = u2
consider u being non zero Element of (TOP-REAL 3) such that
A8: ( P = Dir u & u . 3 = 1 & u1 = |[(u . 1),(u . 2)]| ) by A6;
consider v being non zero Element of (TOP-REAL 3) such that
A9: ( P = Dir v & v . 3 = 1 & u2 = |[(v . 1),(v . 2)]| ) by A7;
|[(u `1),(u `2),(u `3)]| = u by EUCLID_5:3
.= v by A8, A9, Th37
.= |[(v `1),(v `2),(v `3)]| by EUCLID_5:3 ;
then ( u `1 = v `1 & u `2 = v `2 & u `3 = v `3 ) by FINSEQ_1:78;
then ( u . 1 = v `1 & u . 2 = v `2 ) by EUCLID_5:def 1, EUCLID_5:def 2;
then ( u . 1 = v . 1 & u . 2 = v . 2 ) by EUCLID_5:def 1, EUCLID_5:def 2;
hence u1 = u2 by A8, A9; :: thesis: verum