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

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

hence
IncProj (A,o,B) is one-to-one
by FUNCT_1:def 4; :: thesis: verumx1 = 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;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