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) )
assume A1: not o on A ; :: thesis: IncProj A,o,A = id (CHAIN A)
set f = IncProj A,o,A;
A2: dom (IncProj A,o,A) = CHAIN A by A1, Th5;
for x being set st x in CHAIN A holds
(IncProj A,o,A) . x = x

proof

let x be set ; :: 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 x' being Element of the Points of IPP st
( x = x' & x' on A ) ;
hence (IncProj A,o,A) . x = x by A1, PROJRED1:27; :: thesis: verum

end;

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