consider u being Element of (TOP-REAL 3) such that
A1:
not u is zero
and
A2:
P = Dir u
by ANPROJ_1:26;
u . 3 <> 0
by A1, A2, Th67;
then A3:
u `3 <> 0
by EUCLID_5:def 3;
then reconsider r = 1 / (u `3) as non zero Real ;
reconsider v = |[((u `1) / (u `3)),((u `2) / (u `3)),1]| as non zero Element of (TOP-REAL 3) by Th36;
r * u =
(1 / (u `3)) * |[(u `1),(u `2),(u `3)]|
by EUCLID_5:3
.=
|[((1 / (u `3)) * (u `1)),((1 / (u `3)) * (u `2)),((1 / (u `3)) * (u `3))]|
by EUCLID_5:8
.=
|[((u `1) / (u `3)),((1 / (u `3)) * (u `2)),((1 / (u `3)) * (u `3))]|
by XCMPLX_1:99
.=
|[((u `1) / (u `3)),((u `2) / (u `3)),((1 / (u `3)) * (u `3))]|
by XCMPLX_1:99
.=
|[((u `1) / (u `3)),((u `2) / (u `3)),((u `3) / (u `3))]|
by XCMPLX_1:99
.=
v
by A3, XCMPLX_1:60
;
then
are_Prop u,v
by ANPROJ_1:1;
then A4:
P = Dir v
by A1, A2, ANPROJ_1:22;
A5: v . 3 =
v `3
by EUCLID_5:def 3
.=
1
by EUCLID_5:2
;
then
|[(v . 1),(v . 2)]| in circle (0,0,1)
by A4, Th68;
hence
ex b1 being Element of circle (0,0,1) ex u being non zero Element of (TOP-REAL 3) st
( P = Dir u & u . 3 = 1 & b1 = |[(u . 1),(u . 2)]| )
by A4, A5; verum