let P, Q be non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)); ( RP3_to_T2 P = RP3_to_T2 Q implies P = Q )
assume A1:
RP3_to_T2 P = RP3_to_T2 Q
; P = Q
consider u being non zero Element of (TOP-REAL 3) such that
A2:
P = Dir u
and
A3:
u `3 = 1
and
A4:
RP3_to_REAL2 P = |[(u `1),(u `2)]|
by Def05;
consider v being non zero Element of (TOP-REAL 3) such that
A5:
Q = Dir v
and
A6:
v `3 = 1
and
A7:
RP3_to_REAL2 Q = |[(v `1),(v `2)]|
by Def05;
( v `1 = u `1 & v `2 = u `2 & v `3 = u `3 )
by A1, A4, A7, A3, A6, FINSEQ_1:77;
then
|[(u `1),(u `2),(u `3)]| = v
by EUCLID_5:3;
hence
P = Q
by A2, A5, EUCLID_5:3; verum