let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis: for a, b, c, d, q, o, o9, o99, oo9 being POINT of IPP

for O1, O2, O3, A, B, C, O, Q being LINE of IPP st 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,o99,d} on B & {c,d,o9} on C & {a,b,d} on O & {c,oo9} on Q & {a,o,o9} on O1 & {b,o9,oo9} on O2 & {o,oo9,q} on O3 & q on O holds

(IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q))

let a, b, c, d, q, o, o9, o99, oo9 be POINT of IPP; :: thesis: for O1, O2, O3, A, B, C, O, Q being LINE of IPP st 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,o99,d} on B & {c,d,o9} on C & {a,b,d} on O & {c,oo9} on Q & {a,o,o9} on O1 & {b,o9,oo9} on O2 & {o,oo9,q} on O3 & q on O holds

(IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q))

let O1, O2, O3, A, B, C, O, Q be LINE of IPP; :: thesis: ( 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,o99,d} on B & {c,d,o9} on C & {a,b,d} on O & {c,oo9} on Q & {a,o,o9} on O1 & {b,o9,oo9} on O2 & {o,oo9,q} on O3 & q on O implies (IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q)) )

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: (IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q))

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

o9 <> d

then A50: q <> oo9 by A8, A18, A23, A30, A22, INCPROJ:def 4;

A51: not q on Q

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

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

hence (IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q)) by A53, A81, FUNCT_1:2; :: thesis: verum

for O1, O2, O3, A, B, C, O, Q being LINE of IPP st 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,o99,d} on B & {c,d,o9} on C & {a,b,d} on O & {c,oo9} on Q & {a,o,o9} on O1 & {b,o9,oo9} on O2 & {o,oo9,q} on O3 & q on O holds

(IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q))

let a, b, c, d, q, o, o9, o99, oo9 be POINT of IPP; :: thesis: for O1, O2, O3, A, B, C, O, Q being LINE of IPP st 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,o99,d} on B & {c,d,o9} on C & {a,b,d} on O & {c,oo9} on Q & {a,o,o9} on O1 & {b,o9,oo9} on O2 & {o,oo9,q} on O3 & q on O holds

(IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q))

let O1, O2, O3, A, B, C, O, Q be LINE of IPP; :: thesis: ( 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,o99,d} on B & {c,d,o9} on C & {a,b,d} on O & {c,oo9} on Q & {a,o,o9} on O1 & {b,o9,oo9} on O2 & {o,oo9,q} on O3 & q on O implies (IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q)) )

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: (IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q))

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

A49:
a on O
by A13, INCSP_1:2;
assume
q on A
; :: thesis: contradiction

then oo9 on A by A37, A35, A29, A40, INCPROJ:def 4;

hence contradiction by A9, A20, A42, A47, INCPROJ:def 4; :: thesis: verum

end;then oo9 on A by A37, A35, A29, A40, INCPROJ:def 4;

hence contradiction by A9, A20, A42, A47, INCPROJ:def 4; :: thesis: verum

o9 <> d

proof

then
O <> O2
by A2, A32, A21, A49, A34, A28, INCPROJ:def 4;
assume
not o9 <> d
; :: thesis: contradiction

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: verum

end;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: verum

then A50: q <> oo9 by A8, A18, A23, A30, A22, INCPROJ:def 4;

A51: not q on Q

proof

then A52:
dom (IncProj (A,q,Q)) = CHAIN A
by A48, Th4;
assume
q on Q
; :: thesis: contradiction

then o on Q by A42, A35, A29, A50, INCPROJ:def 4;

hence contradiction by A9, A20, A37, A45, INCPROJ:def 4; :: thesis: verum

end;then o on Q by A42, A35, A29, A50, INCPROJ:def 4;

hence contradiction by A9, A20, A37, A45, INCPROJ:def 4; :: thesis: verum

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

A56:
( c on Q & oo9 on Q )
by A14, INCSP_1:1;
assume
not O1 <> O2
; :: thesis: contradiction

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: verum

end;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: verum

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: ( x on A implies ((IncProj (C,b,B)) * (IncProj (A,a,C))) . x = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . x )

assume A61: x on A ; :: thesis: ((IncProj (C,b,B)) * (IncProj (A,a,C))) . x = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . x

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: verum

end;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: ( x on A implies ((IncProj (C,b,B)) * (IncProj (A,a,C))) . x = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . x )

assume A61: x on A ; :: thesis: ((IncProj (C,b,B)) * (IncProj (A,a,C))) . x = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . x

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: verum

A81: now :: thesis: for y being object st y in CHAIN A holds

((IncProj (C,b,B)) * (IncProj (A,a,C))) . y = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . y

dom ((IncProj (C,b,B)) * (IncProj (A,a,C))) = CHAIN A
by A1, A2, A3, A4, A27, PROJRED1:22;((IncProj (C,b,B)) * (IncProj (A,a,C))) . y = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . y

let y be object ; :: thesis: ( y in CHAIN A implies ((IncProj (C,b,B)) * (IncProj (A,a,C))) . y = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . y )

assume y in CHAIN A ; :: thesis: ((IncProj (C,b,B)) * (IncProj (A,a,C))) . y = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . y

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: verum

end;assume y in CHAIN A ; :: thesis: ((IncProj (C,b,B)) * (IncProj (A,a,C))) . y = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . y

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: verum

hence (IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q)) by A53, A81, FUNCT_1:2; :: thesis: verum