let P be Element of BK_model ; REAL2_to_BK (BK_to_REAL2 P) = P
consider u being non zero Element of (TOP-REAL 3) such that
A1:
Dir u = P
and
A2:
u . 3 = 1
and
A3:
BK_to_REAL2 P = |[(u . 1),(u . 2)]|
by Def01;
consider Q being Element of (TOP-REAL 2) such that
A4:
Q = BK_to_REAL2 P
and
A5:
REAL2_to_BK (BK_to_REAL2 P) = Dir |[(Q `1),(Q `2),1]|
by Def02;
A6:
not |[(Q `1),(Q `2),1]| is zero
by EUCLID_5:4, FINSEQ_1:78;
are_Prop |[(Q `1),(Q `2),1]|,u
proof
A7:
(
Q `1 = u . 1 &
Q `2 = u . 2 )
by A3, A4, EUCLID:52;
u =
|[(u `1),(u `2),(u `3)]|
by EUCLID_5:3
.=
|[(u . 1),(u `2),(u `3)]|
by EUCLID_5:def 1
.=
|[(u . 1),(u . 2),(u `3)]|
by EUCLID_5:def 2
.=
|[(u . 1),(u . 2),(u . 3)]|
by EUCLID_5:def 3
;
hence
are_Prop |[(Q `1),(Q `2),1]|,
u
by A2, A7;
verum
end;
hence
REAL2_to_BK (BK_to_REAL2 P) = P
by A1, A5, A6, ANPROJ_1:22; verum