let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis:
let o be POINT of IPP; :: thesis:
let A, B, C be LINE of IPP; :: thesis:
assume that
A1: not o on A and
A2: not o on B and
A3: not o on C ; :: thesis:
set f = IncProj A,o,B;
set g = IncProj C,o,B;
set h = IncProj A,o,C;
A4: dom (IncProj A,o,B) = CHAIN A by A1, A2, Th5;
set X = CHAIN A;
A5: dom (IncProj A,o,C) = CHAIN A by A1, A3, Th5;
A6: 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

let x be POINT of IPP; :: thesis:
assume A7: x on A ; :: thesis:
consider Q1 being LINE of IPP such that
A8: o on Q1 and
A9: x on Q1 by INCPROJ:def 10;
consider x9 being POINT of IPP such that
A10: ( x9 on Q1 & x9 on C ) by INCPROJ:def 14;
A11: (IncProj A,o,C) . x = x9 by A1, A3, A7, A8, A9, A10, PROJRED1:def 1;
consider y being POINT of IPP such that
A12: ( y on Q1 & y on B ) by INCPROJ:def 14;
A13: (IncProj A,o,B) . x = y by A1, A2, A7, A8, A9, A12, PROJRED1:def 1;
x in dom (IncProj A,o,C) by A5, A7;
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 A2, A3, A8, A10, A12, A13, A11, PROJRED1:def 1 ;
hence (IncProj A,o,B) . x = ((IncProj C,o,B) * (IncProj A,o,C)) . x ; :: thesis:

end;

A14: now

let y be set ; :: thesis:
assume y in CHAIN A ; :: thesis:
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 A6; :: thesis:

end;