let IPP be 2-dimensional Desarguesian IncProjSp; for o being POINT of IPP
for A, B being LINE of IPP st not o on A & not o on B holds
IncProj (A,o,B) is one-to-one
let o be POINT of IPP; for A, B being LINE of IPP st not o on A & not o on B holds
IncProj (A,o,B) is one-to-one
let A, B be LINE of IPP; ( not o on A & not o on B implies IncProj (A,o,B) is one-to-one )
set f = IncProj (A,o,B);
assume A1:
( not o on A & not o on B )
; IncProj (A,o,B) is one-to-one
now for x1, x2 being object st x1 in dom (IncProj (A,o,B)) & x2 in dom (IncProj (A,o,B)) & (IncProj (A,o,B)) . x1 = (IncProj (A,o,B)) . x2 holds
x1 = x2let x1,
x2 be
object ;
( x1 in dom (IncProj (A,o,B)) & x2 in dom (IncProj (A,o,B)) & (IncProj (A,o,B)) . x1 = (IncProj (A,o,B)) . x2 implies x1 = x2 )assume that A2:
x1 in dom (IncProj (A,o,B))
and A3:
x2 in dom (IncProj (A,o,B))
and A4:
(IncProj (A,o,B)) . x1 = (IncProj (A,o,B)) . x2
;
x1 = x2
x1 in CHAIN A
by A1, A2, Th4;
then consider a being
POINT of
IPP such that A5:
x1 = a
and A6:
a on A
;
x2 in CHAIN A
by A1, A3, Th4;
then consider b being
POINT of
IPP such that A7:
x2 = b
and A8:
b on A
;
reconsider x =
(IncProj (A,o,B)) . a,
y =
(IncProj (A,o,B)) . b as
POINT of
IPP by A1, A6, A8, PROJRED1:19;
x = y
by A4, A5, A7;
hence
x1 = x2
by A1, A5, A6, A7, A8, PROJRED1:23;
verum end;
hence
IncProj (A,o,B) is one-to-one
by FUNCT_1:def 4; verum