let IPP be 2-dimensional Desarguesian IncProjSp; 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; 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; ( not o on A implies IncProj (A,o,A) = id (CHAIN A) )
set f = IncProj (A,o,A);
assume A1:
not o on A
; IncProj (A,o,A) = id (CHAIN A)
A2:
for x being object st x in CHAIN A holds
(IncProj (A,o,A)) . x = x
dom (IncProj (A,o,A)) = CHAIN A
by A1, Th4;
hence
IncProj (A,o,A) = id (CHAIN A)
by A2, FUNCT_1:17; verum