let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis: for o being POINT of IPP
for A, B, C being LINE of IPP st not o on A & not o on B & not o on C holds
(IncProj (C,o,B)) * (IncProj (A,o,C)) = IncProj (A,o,B)
let o be POINT of IPP; :: thesis: for A, B, C being LINE of IPP st not o on A & not o on B & not o on C holds
(IncProj (C,o,B)) * (IncProj (A,o,C)) = IncProj (A,o,B)
let A, B, C be LINE of IPP; :: thesis: ( not o on A & not o on B & not o on C implies (IncProj (C,o,B)) * (IncProj (A,o,C)) = IncProj (A,o,B) )
assume that
A1: not o on A and
A2: not o on B and
A3: not o on C ; :: thesis: (IncProj (C,o,B)) * (IncProj (A,o,C)) = IncProj (A,o,B)
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, Th4;
set X = CHAIN A;
A5: dom (IncProj (A,o,C)) = CHAIN A by A1, A3, Th4;
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

proof

let x be POINT of IPP; :: thesis: ( x on A implies (IncProj (A,o,B)) . x = ((IncProj (C,o,B)) * (IncProj (A,o,C))) . x )
assume A7: x on A ; :: thesis: (IncProj (A,o,B)) . x = ((IncProj (C,o,B)) * (IncProj (A,o,C))) . x
consider Q1 being LINE of IPP such that
A8: o on Q1 and
A9: x on Q1 by INCPROJ:def 5;
consider x9 being POINT of IPP such that
A10: ( x9 on Q1 & x9 on C ) by INCPROJ:def 9;
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 9;
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:13
.= (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: verum

end;

A14: now :: thesis: for y being object st y in CHAIN A holds
((IncProj (C,o,B)) * (IncProj (A,o,C))) . y = (IncProj (A,o,B)) . y

let y be object ; :: thesis: ( y in CHAIN A implies ((IncProj (C,o,B)) * (IncProj (A,o,C))) . y = (IncProj (A,o,B)) . y )
assume y in CHAIN A ; :: thesis: ((IncProj (C,o,B)) * (IncProj (A,o,C))) . y = (IncProj (A,o,B)) . y
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: verum

end;

dom ((IncProj (C,o,B)) * (IncProj (A,o,C))) = CHAIN A by A1, A2, A3, A5, PROJRED1:22;
hence (IncProj (C,o,B)) * (IncProj (A,o,C)) = IncProj (A,o,B) by A4, A14, FUNCT_1:2; :: thesis: verum