let P1, P2 be Element of inside_of_circle (0,0,1); ( ex u being non zero Element of (TOP-REAL 3) st
( Dir u = P & u . 3 = 1 & P1 = |[(u . 1),(u . 2)]| ) & ex u being non zero Element of (TOP-REAL 3) st
( Dir u = P & u . 3 = 1 & P2 = |[(u . 1),(u . 2)]| ) implies P1 = P2 )
assume that
A18:
ex u being non zero Element of (TOP-REAL 3) st
( Dir u = P & u . 3 = 1 & P1 = |[(u . 1),(u . 2)]| )
and
A19:
ex u being non zero Element of (TOP-REAL 3) st
( Dir u = P & u . 3 = 1 & P2 = |[(u . 1),(u . 2)]| )
; P1 = P2
consider u being non zero Element of (TOP-REAL 3) such that
A20:
( Dir u = P & u . 3 = 1 & P1 = |[(u . 1),(u . 2)]| )
by A18;
consider v being non zero Element of (TOP-REAL 3) such that
A21:
( Dir v = P & v . 3 = 1 & P2 = |[(v . 1),(v . 2)]| )
by A19;
are_Prop u,v
by A20, A21, ANPROJ_1:22;
then consider a being Real such that
a <> 0
and
A22:
u = a * v
by ANPROJ_1:1;
1 =
a * (v . 3)
by A20, A22, RVSUM_1:44
.=
a
by A21
;
then
u = v
by A22, RVSUM_1:52;
hence
P1 = P2
by A20, A21; verum