let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: IncProj (A,o,B) is one-to-one

now :: thesis: 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 = x2

let x1, x2 be object ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

end;

hence IncProj (A,o,B) is one-to-one by FUNCT_1:def 4; :: thesis: verum