let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis:
let a, b, c, q, d, p, pp' be POINT of IPP; :: thesis:
let A, B, C, Q, O, O1, O2, O3 be LINE of IPP; :: thesis:
assume A1: ( not a on A & not b on B & not a on C & not b on C & not A,B,C are_concurrent & c on A & c on C & c on Q & not b on Q & A <> Q & a <> b & b <> q & a on O & b on O & not B,C,O are_concurrent & d on C & d on B & a on O1 & d on O1 & p on A & p on O1 & q on O & q on O2 & p on O2 & pp' on O2 & d on O3 & b on O3 & pp' on O3 & pp' on Q & Q <> C & q <> a & not q on A & not q on Q ) ; :: thesis:
then c <> d by Def1;
then p <> c by A1, INCPROJ:def 9;
then A2: pp' <> p by A1, INCPROJ:def 9;
A3: O1 <> O2

proof

assume not O1 <> O2 ; :: thesis:
then d on O by A1, INCPROJ:def 9;
hence contradiction by A1, Def1; :: thesis:

end;

set f = IncProj A,a,C;
set g = IncProj C,b,B;
set g1 = IncProj Q,b,B;
set f1 = IncProj A,q,Q;
A4: ( dom (IncProj A,a,C) = CHAIN A & dom (IncProj C,b,B) = CHAIN C & dom (IncProj A,q,Q) = CHAIN A & dom (IncProj Q,b,B) = CHAIN Q ) by A1, Th5;
A5: for x being POINT of IPP st x on A holds
((IncProj C,b,B) * (IncProj A,a,C)) . x = ((IncProj Q,b,B) * (IncProj A,q,Q)) . x

proof

let x be POINT of IPP; :: thesis:
assume A6: x on A ; :: thesis:
consider Q1 being LINE of IPP such that
A7: ( a on Q1 & x on Q1 ) by INCPROJ:def 10;
consider x' being POINT of IPP such that
A8: ( x' on Q1 & x' on C ) by INCPROJ:def 14;
consider Q3 being LINE of IPP such that
A9: ( q on Q3 & x on Q3 ) by INCPROJ:def 10;
consider y being POINT of IPP such that
A10: ( y on Q3 & y on Q ) by INCPROJ:def 14;

A11: now

assume A12: p = x ; :: thesis:
A13: ( (IncProj A,a,C) . p = d & (IncProj C,b,B) . d = d ) by A1, PROJRED1:def 1;
A14: ( (IncProj A,q,Q) . p = pp' & (IncProj Q,b,B) . pp' = d ) by A1, PROJRED1:def 1;
A15: ( x in dom (IncProj A,a,C) & d in dom (IncProj C,b,B) & pp' in dom (IncProj Q,b,B) & x in dom (IncProj A,q,Q) ) by A1, A4, A6;
then ((IncProj C,b,B) * (IncProj A,a,C)) . x = (IncProj Q,b,B) . ((IncProj A,q,Q) . x) by A12, A13, A14, FUNCT_1:23
.= ((IncProj Q,b,B) * (IncProj A,q,Q)) . x by A15, FUNCT_1:23 ;
hence ((IncProj C,b,B) * (IncProj A,a,C)) . x = ((IncProj Q,b,B) * (IncProj A,q,Q)) . x ; :: thesis:

end;

now

assume A16: p <> x ; :: thesis:
( {p,x,c} on A & {p,d,a} on O1 & {p,pp',q} on O2 & {pp',d,b} on O3 & {pp',y,c} on Q & {d,x',c} on C & {b,a,q} on O & {x,y,q} on Q3 & {x,x',a} on Q1 & A,O1,O2 are_mutually_different ) by A1, A3, A6, A7, A8, A9, A10, INCSP_1:12, ZFMISC_1:def 5;
then consider R being LINE of IPP such that
A17: {y,x',b} on R by A1, A2, A16, PROJRED1:14;
consider x'' being POINT of IPP such that
A18: ( x'' on R & x'' on B ) by INCPROJ:def 14;
A19: ( y on R & x' on R & b on R ) by A17, INCSP_1:12;
then A20: ( (IncProj A,a,C) . x = x' & (IncProj C,b,B) . x' = x'' ) by A1, A6, A7, A8, A18, PROJRED1:def 1;
A21: ( (IncProj A,q,Q) . x = y & (IncProj Q,b,B) . y = x'' ) by A1, A6, A9, A10, A18, A19, PROJRED1:def 1;
A22: ( x in dom (IncProj A,a,C) & x' in dom (IncProj C,b,B) & y in dom (IncProj Q,b,B) & x in dom (IncProj A,q,Q) ) by A4, A6, A8, A10;
then ((IncProj C,b,B) * (IncProj A,a,C)) . x = (IncProj Q,b,B) . ((IncProj A,q,Q) . x) by A20, A21, FUNCT_1:23
.= ((IncProj Q,b,B) * (IncProj A,q,Q)) . x by A22, FUNCT_1:23 ;
hence ((IncProj C,b,B) * (IncProj A,a,C)) . x = ((IncProj Q,b,B) * (IncProj A,q,Q)) . x ; :: thesis:

end;

hence ((IncProj C,b,B) * (IncProj A,a,C)) . x = ((IncProj Q,b,B) * (IncProj A,q,Q)) . x by A11; :: thesis:

end;

set X = CHAIN A;
A23: ( dom ((IncProj C,b,B) * (IncProj A,a,C)) = CHAIN A & dom ((IncProj Q,b,B) * (IncProj A,q,Q)) = CHAIN A ) by A1, A4, PROJRED1:25;

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,b,B) * (IncProj A,a,C)) . y = ((IncProj Q,b,B) * (IncProj A,q,Q)) . y by A5; :: thesis:

end;

hence (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q) by A23, FUNCT_1:9; :: thesis: