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 ;
x = y by A4, A5, A7;
hence x1 = x2 by ; :: thesis: verum
end;
hence IncProj (A,o,B) is one-to-one by FUNCT_1:def 4; :: thesis: verum