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
proof
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;
dom (IncProj (A,o,A)) = CHAIN A by A1, Th4;
hence IncProj (A,o,A) = id (CHAIN A) by A2, FUNCT_1:17; :: thesis: verum