let P be POINT of TarskiEuclid2Space; ( Tn2TR P is Element of inside_of_circle (0,0,1) implies BK_to_T2 (T2_to_BK P) = P )
assume
Tn2TR P is Element of inside_of_circle (0,0,1)
; BK_to_T2 (T2_to_BK P) = P
then consider u being non zero Element of (TOP-REAL 3) such that
A1:
T2_to_BK P = Dir u
and
A2:
u `3 = 1
and
A3:
Tn2TR P = |[(u `1),(u `2)]|
by Def02;
reconsider Q9 = T2_to_BK P as Element of BK-model-Plane ;
reconsider Q = T2_to_BK P as Element of BK_model ;
consider p being Element of BK_model such that
A4:
Q9 = p
and
A5:
BK_to_T2 Q9 = BK_to_REAL2 p
by Def01;
consider v being non zero Element of (TOP-REAL 3) such that
A6:
Dir v = p
and
A7:
v . 3 = 1
and
A8:
BK_to_REAL2 p = |[(v . 1),(v . 2)]|
by BKMODEL2:def 2;
are_Prop u,v
by A4, A6, A1, ANPROJ_1:22;
then consider a being Real such that
a <> 0
and
A9:
u = a * v
by ANPROJ_1:1;
A10: 1 =
a * (v `3)
by A2, A9, EUCLID_5:9
.=
a * 1
by A7, EUCLID_5:def 3
.=
a
;
|[(u `1),(u `2),(u `3)]| =
u
by EUCLID_5:3
.=
|[(1 * (v `1)),(1 * (v `2)),(1 * (v `3))]|
by A9, A10, EUCLID_5:7
;
then
( u `1 = v `1 & u `2 = v `2 )
by FINSEQ_1:78;
then
( u `1 = v . 1 & u `2 = v . 2 )
by EUCLID_5:def 1, EUCLID_5:def 2;
hence
BK_to_T2 (T2_to_BK P) = P
by A5, A8, A3; verum