let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis: for o being POINT of IPP

for A being LINE of IPP st not o on A holds

IncProj (A,o,A) = id (CHAIN A)

let o be POINT of IPP; :: thesis: for A being LINE of IPP st not o on A holds

IncProj (A,o,A) = id (CHAIN A)

let A be LINE of IPP; :: thesis: ( not o on A implies IncProj (A,o,A) = id (CHAIN A) )

set f = IncProj (A,o,A);

assume A1: not o on A ; :: thesis: IncProj (A,o,A) = id (CHAIN A)

A2: for x being object st x in CHAIN A holds

(IncProj (A,o,A)) . x = x

hence IncProj (A,o,A) = id (CHAIN A) by A2, FUNCT_1:17; :: thesis: verum

for A being LINE of IPP st not o on A holds

IncProj (A,o,A) = id (CHAIN A)

let o be POINT of IPP; :: thesis: for A being LINE of IPP st not o on A holds

IncProj (A,o,A) = id (CHAIN A)

let A be LINE of IPP; :: thesis: ( not o on A implies IncProj (A,o,A) = id (CHAIN A) )

set f = IncProj (A,o,A);

assume A1: not o on A ; :: thesis: IncProj (A,o,A) = id (CHAIN A)

A2: for x being object st x in CHAIN A holds

(IncProj (A,o,A)) . x = x

proof

dom (IncProj (A,o,A)) = CHAIN A
by A1, Th4;
let x be object ; :: thesis: ( x in CHAIN A implies (IncProj (A,o,A)) . x = x )

assume x in CHAIN A ; :: thesis: (IncProj (A,o,A)) . x = x

then ex x9 being Element of the Points of IPP st

( x = x9 & x9 on A ) ;

hence (IncProj (A,o,A)) . x = x by A1, PROJRED1:24; :: thesis: verum

end;assume x in CHAIN A ; :: thesis: (IncProj (A,o,A)) . x = x

then ex x9 being Element of the Points of IPP st

( x = x9 & x9 on A ) ;

hence (IncProj (A,o,A)) . x = x by A1, PROJRED1:24; :: thesis: verum

hence IncProj (A,o,A) = id (CHAIN A) by A2, FUNCT_1:17; :: thesis: verum