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

let x1, x2 be set ; :: 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, Th5;
then consider a being POINT of IPP such that
A5: x1 = a and
A6: a on A ;
x2 in CHAIN A by A1, A3, Th5;
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:22;
x = y by A4, A5, A7;
hence x1 = x2 by A1, A5, A6, A7, A8, PROJRED1:26; :: thesis: verum

end;

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