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 )
assume A1: ( not o on A & not o on B ) ; :: thesis: IncProj A,o,B is one-to-one
set f = IncProj A,o,B;

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) & x2 in dom (IncProj A,o,B) ) and
A3: (IncProj A,o,B) . x1 = (IncProj A,o,B) . x2 ; :: thesis: x1 = x2
A4: ( x1 in CHAIN A & x2 in CHAIN A ) by A1, A2, Th5;
then consider a being POINT of IPP such that
A5: ( x1 = a & a on A ) ;
consider b being POINT of IPP such that
A6: ( x2 = b & b on A ) by A4;
reconsider x = (IncProj A,o,B) . a, y = (IncProj A,o,B) . b as POINT of IPP by A1, A5, A6, PROJRED1:22;
x = y by A3, A5, A6;
hence x1 = x2 by A1, A5, A6, PROJRED1:26; :: thesis: verum

end;

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