let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis: for o being POINT of IPP
for A, B, C being LINE of IPP st not o on A & not o on B & not o on C holds
(IncProj C,o,B) * (IncProj A,o,C) = IncProj A,o,B
let o be POINT of IPP; :: thesis: for A, B, C being LINE of IPP st not o on A & not o on B & not o on C holds
(IncProj C,o,B) * (IncProj A,o,C) = IncProj A,o,B
let A, B, C be LINE of IPP; :: thesis: ( not o on A & not o on B & not o on C implies (IncProj C,o,B) * (IncProj A,o,C) = IncProj A,o,B )
assume A1: ( not o on A & not o on B & not o on C ) ; :: thesis: (IncProj C,o,B) * (IncProj A,o,C) = IncProj A,o,B
set f = IncProj A,o,B;
set g = IncProj C,o,B;
set h = IncProj A,o,C;
A2: ( dom (IncProj A,o,B) = CHAIN A & dom (IncProj C,o,B) = CHAIN C & dom (IncProj A,o,C) = CHAIN A ) by A1, Th5;
A3: for x being POINT of IPP st x on A holds
(IncProj A,o,B) . x = ((IncProj C,o,B) * (IncProj A,o,C)) . x

proof

let x be POINT of IPP; :: thesis: ( x on A implies (IncProj A,o,B) . x = ((IncProj C,o,B) * (IncProj A,o,C)) . x )
assume A4: x on A ; :: thesis: (IncProj A,o,B) . x = ((IncProj C,o,B) * (IncProj A,o,C)) . x
consider Q1 being LINE of IPP such that
A5: ( o on Q1 & x on Q1 ) by INCPROJ:def 10;
consider x' being POINT of IPP such that
A6: ( x' on Q1 & x' on C ) by INCPROJ:def 14;
consider y being POINT of IPP such that
A7: ( y on Q1 & y on B ) by INCPROJ:def 14;
A8: (IncProj A,o,B) . x = y by A1, A4, A5, A7, PROJRED1:def 1;
A9: (IncProj A,o,C) . x = x' by A1, A4, A5, A6, PROJRED1:def 1;
( x in dom (IncProj A,o,B) & x' in dom (IncProj C,o,B) & x in dom (IncProj A,o,C) ) by A2, A4, A6;
then ((IncProj C,o,B) * (IncProj A,o,C)) . x = (IncProj C,o,B) . ((IncProj A,o,C) . x) by FUNCT_1:23
.= (IncProj A,o,B) . x by A1, A5, A6, A7, A8, A9, PROJRED1:def 1 ;
hence (IncProj A,o,B) . x = ((IncProj C,o,B) * (IncProj A,o,C)) . x ; :: thesis: verum

end;

set X = CHAIN A;
A10: ( dom ((IncProj C,o,B) * (IncProj A,o,C)) = CHAIN A & dom (IncProj A,o,B) = CHAIN A ) by A1, A2, PROJRED1:25;

now

let y be set ; :: thesis: ( y in CHAIN A implies ((IncProj C,o,B) * (IncProj A,o,C)) . y = (IncProj A,o,B) . y )
assume y in CHAIN A ; :: thesis: ((IncProj C,o,B) * (IncProj A,o,C)) . y = (IncProj A,o,B) . y
then ex x being POINT of IPP st
( y = x & x on A ) ;
hence ((IncProj C,o,B) * (IncProj A,o,C)) . y = (IncProj A,o,B) . y by A3; :: thesis: verum

end;

hence (IncProj C,o,B) * (IncProj A,o,C) = IncProj A,o,B by A10, FUNCT_1:9; :: thesis: verum