let Q be Element of inside_of_circle (0,0,1); BK_to_REAL2 (REAL2_to_BK Q) = Q
consider P being Element of (TOP-REAL 2) such that
A1:
P = Q
and
A2:
REAL2_to_BK Q = Dir |[(P `1),(P `2),1]|
by Def02;
consider u being non zero Element of (TOP-REAL 3) such that
A3:
Dir u = REAL2_to_BK Q
and
A4:
u . 3 = 1
and
A5:
BK_to_REAL2 (REAL2_to_BK Q) = |[(u . 1),(u . 2)]|
by Def01;
not |[(P `1),(P `2),1]| is zero
by EUCLID_5:4, FINSEQ_1:78;
then
are_Prop |[(P `1),(P `2),1]|,u
by A2, A3, ANPROJ_1:22;
then consider a being Real such that
a <> 0
and
A6:
|[(P `1),(P `2),1]| = a * u
by ANPROJ_1:1;
A7: a =
a * (u . 3)
by A4
.=
(a * u) . 3
by RVSUM_1:44
.=
|[(P `1),(P `2),1]| `3
by A6, EUCLID_5:def 3
.=
1
by EUCLID_5:2
;
A8:
|[(P `1),(P `2),1]| = u
by A7, RVSUM_1:52, A6;
then A9: P `1 =
u `1
by EUCLID_5:2
.=
u . 1
by EUCLID_5:def 1
;
P `2 =
u `2
by A8, EUCLID_5:2
.=
u . 2
by EUCLID_5:def 2
;
hence
BK_to_REAL2 (REAL2_to_BK Q) = Q
by A9, A5, A1, EUCLID:53; verum