let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis:
let a, b, c, d, q, o, o9, o99, oo9 be POINT of IPP; :: thesis:
let O1, O2, O3, A, B, C, O, Q be LINE of IPP; :: thesis:
assume that
A1: not a on A and
A2: not a on C and
A3: not b on B and
A4: not b on C and
A5: not b on Q and
A6: not A,B,C are_concurrent and
A7: a <> b and
A8: b <> q and
A9: A <> Q and
A10: {c,o} on A and
A11: {o,o99,d} on B and
A12: {c,d,o9} on C and
A13: {a,b,d} on O and
A14: {c,oo9} on Q and
A15: {a,o,o9} on O1 and
A16: {b,o9,oo9} on O2 and
A17: {o,oo9,q} on O3 and
A18: q on O ; :: thesis:
A19: o on A by A10, INCSP_1:1;
A20: ( c on A & c on Q ) by A10, A14, INCSP_1:1;
A21: o9 on C by A12, INCSP_1:2;
A22: oo9 on O2 by A16, INCSP_1:2;
A23: b on O by A13, INCSP_1:2;
A24: q on O3 by A17, INCSP_1:2;
A25: ( o on O3 & oo9 on O3 ) by A17, INCSP_1:2;
set X = CHAIN A;
set f = IncProj (A,a,C);
set g = IncProj (C,b,B);
set f1 = IncProj (A,q,Q);
set g1 = IncProj (Q,b,B);
A26: o on B by A11, INCSP_1:2;
A27: dom (IncProj (A,a,C)) = CHAIN A by A1, A2, Th4;
A28: o9 on O2 by A16, INCSP_1:2;
A29: q on O3 by A17, INCSP_1:2;
A30: b on O2 by A16, INCSP_1:2;
A31: o on B by A11, INCSP_1:2;
A32: d on C by A12, INCSP_1:2;
then A33: o <> d by A6, A19, A31;
A34: d on O by A13, INCSP_1:2;
A35: ( o on O3 & oo9 on O3 ) by A17, INCSP_1:2;
A36: o9 on O1 by A15, INCSP_1:2;
A37: o on A by A10, INCSP_1:1;
A38: a on O1 by A15, INCSP_1:2;
A39: d on B by A11, INCSP_1:2;
then A40: q <> o by A3, A18, A31, A23, A34, A33, INCPROJ:def 4;
A41: c on C by A12, INCSP_1:2;
A42: oo9 on Q by A14, INCSP_1:1;
A43: o on O1 by A15, INCSP_1:2;
A44: c on A by A10, INCSP_1:1;
then A45: o <> c by A6, A31, A41;
then A46: o9 <> c by A1, A44, A19, A38, A43, A36, INCPROJ:def 4;
then A47: c <> oo9 by A4, A41, A21, A30, A28, A22, INCPROJ:def 4;
A48: not q on A

proof

assume q on A ; :: thesis:
then oo9 on A by A37, A35, A29, A40, INCPROJ:def 4;
hence contradiction by A9, A20, A42, A47, INCPROJ:def 4; :: thesis:

end;

A49: a on O by A13, INCSP_1:2;
o9 <> d

proof

assume not o9 <> d ; :: thesis:
then O1 = O by A2, A32, A49, A34, A38, A36, INCPROJ:def 4;
hence contradiction by A3, A31, A39, A23, A34, A43, A33, INCPROJ:def 4; :: thesis:

end;

then O <> O2 by A2, A32, A21, A49, A34, A28, INCPROJ:def 4;
then A50: q <> oo9 by A8, A18, A23, A30, A22, INCPROJ:def 4;
A51: not q on Q

proof

assume q on Q ; :: thesis:
then o on Q by A42, A35, A29, A50, INCPROJ:def 4;
hence contradiction by A9, A20, A37, A45, INCPROJ:def 4; :: thesis:

end;

then A52: dom (IncProj (A,q,Q)) = CHAIN A by A48, Th4;
then A53: dom ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) = CHAIN A by A3, A5, A48, A51, PROJRED1:22;
A54: ( d on B & d on O ) by A11, A13, INCSP_1:2;
A55: O1 <> O2

proof

assume not O1 <> O2 ; :: thesis:
then o on O by A7, A49, A23, A38, A43, A30, INCPROJ:def 4;
then O = B by A54, A26, A33, INCPROJ:def 4;
hence contradiction by A3, A13, INCSP_1:2; :: thesis:

end;

A56: ( c on Q & oo9 on Q ) by A14, INCSP_1:1;
A57: 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

A58: ( {o9,b,oo9} on O2 & {o9,o,a} on O1 ) by A38, A43, A36, A30, A28, A22, INCSP_1:2;
A59: ( {o,q,oo9} on O3 & {b,q,a} on O ) by A18, A49, A23, A25, A24, INCSP_1:2;
A60: O2,O1,C are_mutually_distinct by A2, A4, A38, A30, A55, ZFMISC_1:def 5;
let x be POINT of IPP; :: thesis:
assume A61: x on A ; :: thesis:
A62: {c,o,x} on A by A44, A19, A61, INCSP_1:2;
A63: x in dom (IncProj (A,q,Q)) by A52, A61;
A64: x in dom (IncProj (A,a,C)) by A27, A61;
consider Q1 being LINE of IPP such that
A65: ( a on Q1 & x on Q1 ) by INCPROJ:def 5;
consider x9 being POINT of IPP such that
A66: x9 on Q1 and
A67: x9 on C by INCPROJ:def 9;
A68: {x,a,x9} on Q1 by A65, A66, INCSP_1:2;
A69: {o9,c,x9} on C by A41, A21, A67, INCSP_1:2;
consider Q2 being LINE of IPP such that
A70: x9 on Q2 and
A71: b on Q2 by INCPROJ:def 5;
consider y being POINT of IPP such that
A72: y on Q and
A73: y on Q2 by INCPROJ:def 9;
A74: {c,y,oo9} on Q by A56, A72, INCSP_1:2;
{b,y,x9} on Q2 by A70, A71, A73, INCSP_1:2;
then consider R being LINE of IPP such that
A75: {y,q,x} on R by A1, A2, A4, A19, A21, A46, A58, A69, A62, A74, A68, A59, A60, PROJRED1:12;
A76: x on R by A75, INCSP_1:2;
( y on R & q on R ) by A75, INCSP_1:2;
then A77: (IncProj (A,q,Q)) . x = y by A48, A51, A61, A72, A76, PROJRED1:def 1;
consider x99 being POINT of IPP such that
A78: ( x99 on Q2 & x99 on B ) by INCPROJ:def 9;
A79: (IncProj (Q,b,B)) . y = x99 by A3, A5, A71, A78, A72, A73, PROJRED1:def 1;
A80: (IncProj (C,b,B)) . x9 = x99 by A3, A4, A67, A70, A71, A78, PROJRED1:def 1;
(IncProj (A,a,C)) . x = x9 by A1, A2, A61, A65, A66, A67, PROJRED1:def 1;
then ((IncProj (C,b,B)) * (IncProj (A,a,C))) . x = (IncProj (Q,b,B)) . ((IncProj (A,q,Q)) . x) by A80, A77, A79, A64, FUNCT_1:13
.= ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . x by A63, FUNCT_1:13 ;
hence ((IncProj (C,b,B)) * (IncProj (A,a,C))) . x = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . x ; :: thesis:

end;

A81: now :: thesis:

let y be object ; :: 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 A57; :: thesis:

end;

dom ((IncProj (C,b,B)) * (IncProj (A,a,C))) = CHAIN A by A1, A2, A3, A4, A27, PROJRED1:22;
hence (IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q)) by A53, A81, FUNCT_1:2; :: thesis: