let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis:
let a, b, q, c, o, o'', d, o', oo' be POINT of IPP; :: thesis:
let A, C, B, Q, O, O1, O2, O3 be LINE of IPP; :: thesis:
assume A1: ( not a on A & not a on C & not b on B & not b on C & not b on Q & not A,B,C are_concurrent & a <> b & b <> q & A <> Q & {c,o} on A & {o,o'',d} on B & {c,d,o'} on C & {a,b,d} on O & {c,oo'} on Q & {a,o,o'} on O1 & {b,o',oo'} on O2 & {o,oo',q} on O3 & q on O ) ; :: thesis:
then A2: ( not a on A & not a on C & not b on B & not b on C & not b on Q & not A,B,C are_concurrent & a <> b & b <> q & A <> Q & c on A & o on A & o on B & o'' on B & d on B & c on C & d on C & o' on C & a on O & b on O & d on O & c on Q & oo' on Q & a on O1 & o on O1 & o' on O1 & b on O2 & o' on O2 & oo' on O2 & o on O3 & oo' on O3 & q on O3 & q on O ) by INCSP_1:11, INCSP_1:12;
A3: ( c on A & c on C & c on Q ) by A1, INCSP_1:11, INCSP_1:12;
A4: ( d on B & d on C & d on O ) by A1, INCSP_1:12;
A5: ( o on A & o on B ) by A1, INCSP_1:11, INCSP_1:12;
A6: ( oo' on Q & oo' on O2 ) by A1, INCSP_1:11, INCSP_1:12;
A7: ( o on O3 & oo' on O3 ) by A1, INCSP_1:12;
A8: ( q on O3 & q on O ) by A1, INCSP_1:12;
A9: o <> c by A2, Def1;
then A10: o' <> c by A2, INCPROJ:def 9;
A11: o <> d by A2, Def1;
A12: O1 <> O2

proof

assume not O1 <> O2 ; :: thesis:
then o on O by A2, INCPROJ:def 9;
then O = B by A4, A5, A11, INCPROJ:def 9;
hence contradiction by A1, INCSP_1:12; :: thesis:

end;

A13: q <> o by A2, A11, INCPROJ:def 9;
A14: c <> oo' by A2, A10, INCPROJ:def 9;
A15: not q on A

proof

assume q on A ; :: thesis:
then oo' on A by A5, A7, A8, A13, INCPROJ:def 9;
hence contradiction by A1, A3, A6, A14, INCPROJ:def 9; :: thesis:

end;

o' <> d

proof

assume not o' <> d ; :: thesis:
then O1 = O by A2, INCPROJ:def 9;
hence contradiction by A2, A11, INCPROJ:def 9; :: thesis:

end;

then O <> O2 by A2, INCPROJ:def 9;
then A16: q <> oo' by A2, INCPROJ:def 9;
A17: not q on Q

proof

assume q on Q ; :: thesis:
then o on Q by A6, A7, A8, A16, INCPROJ:def 9;
hence contradiction by A1, A3, A5, A9, INCPROJ:def 9; :: thesis:

end;

set f = IncProj A,a,C;
set g = IncProj C,b,B;
set f1 = IncProj A,q,Q;
set g1 = IncProj Q,b,B;
A18: ( 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, A15, A17, Th5;
A19: 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 A20: x on A ; :: thesis:
consider Q1 being LINE of IPP such that
A21: ( a on Q1 & x on Q1 ) by INCPROJ:def 10;
consider x' being POINT of IPP such that
A22: ( x' on Q1 & x' on C ) by INCPROJ:def 14;
consider Q2 being LINE of IPP such that
A23: ( x' on Q2 & b on Q2 ) by INCPROJ:def 10;
consider x'' being POINT of IPP such that
A24: ( x'' on Q2 & x'' on B ) by INCPROJ:def 14;
consider y being POINT of IPP such that
A25: ( y on Q & y on Q2 ) by INCPROJ:def 14;
( {o',b,oo'} on O2 & {o',o,a} on O1 & {o',c,x'} on C & {c,o,x} on A & {c,y,oo'} on Q & {o,q,oo'} on O3 & {x,a,x'} on Q1 & {b,y,x'} on Q2 & {b,q,a} on O & O2,O1,C are_mutually_different ) by A2, A12, A20, A21, A22, A23, A25, INCSP_1:12, ZFMISC_1:def 5;
then consider R being LINE of IPP such that
A26: {y,q,x} on R by A2, A10, PROJRED1:14;
A27: ( y on R & q on R & x on R ) by A26, INCSP_1:12;
A28: ( (IncProj A,a,C) . x = x' & (IncProj C,b,B) . x' = x'' ) by A1, A20, A21, A22, A23, A24, PROJRED1:def 1;
A29: ( (IncProj A,q,Q) . x = y & (IncProj Q,b,B) . y = x'' ) by A1, A15, A17, A20, A23, A24, A25, A27, PROJRED1:def 1;
A30: ( 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 A18, A20, A22, A25;
then ((IncProj C,b,B) * (IncProj A,a,C)) . x = (IncProj Q,b,B) . ((IncProj A,q,Q) . x) by A28, A29, FUNCT_1:23
.= ((IncProj Q,b,B) * (IncProj A,q,Q)) . x by A30, FUNCT_1:23 ;
hence ((IncProj C,b,B) * (IncProj A,a,C)) . x = ((IncProj Q,b,B) * (IncProj A,q,Q)) . x ; :: thesis:

end;

set X = CHAIN A;
A31: ( dom ((IncProj C,b,B) * (IncProj A,a,C)) = CHAIN A & dom ((IncProj Q,b,B) * (IncProj A,q,Q)) = CHAIN A ) by A1, A15, A17, A18, 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 A19; :: thesis:

end;

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