let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis: for p, q being POINT of IPP
for K, L, R being LINE of IPP st not p on K & not p on L & not q on L & not q on R holds
( dom ((IncProj L,q,R) * (IncProj K,p,L)) = dom (IncProj K,p,L) & rng ((IncProj L,q,R) * (IncProj K,p,L)) = rng (IncProj L,q,R) )
let p, q be POINT of IPP; :: thesis: for K, L, R being LINE of IPP st not p on K & not p on L & not q on L & not q on R holds
( dom ((IncProj L,q,R) * (IncProj K,p,L)) = dom (IncProj K,p,L) & rng ((IncProj L,q,R) * (IncProj K,p,L)) = rng (IncProj L,q,R) )
let K, L, R be LINE of IPP; :: thesis: ( not p on K & not p on L & not q on L & not q on R implies ( dom ((IncProj L,q,R) * (IncProj K,p,L)) = dom (IncProj K,p,L) & rng ((IncProj L,q,R) * (IncProj K,p,L)) = rng (IncProj L,q,R) ) )
assume that
A1: ( not p on K & not p on L ) and
A2: ( not q on L & not q on R ) ; :: thesis: ( dom ((IncProj L,q,R) * (IncProj K,p,L)) = dom (IncProj K,p,L) & rng ((IncProj L,q,R) * (IncProj K,p,L)) = rng (IncProj L,q,R) )
for x being set holds
( x in dom ((IncProj L,q,R) * (IncProj K,p,L)) iff x in dom (IncProj K,p,L) )

proof

let x be set ; :: thesis: ( x in dom ((IncProj L,q,R) * (IncProj K,p,L)) iff x in dom (IncProj K,p,L) )
( x in dom (IncProj K,p,L) implies x in dom ((IncProj L,q,R) * (IncProj K,p,L)) )

proof

assume A3: x in dom (IncProj K,p,L) ; :: thesis: x in dom ((IncProj L,q,R) * (IncProj K,p,L))
then reconsider x9 = x as POINT of IPP ;
consider A being LINE of IPP such that
A4: ( x9 on A & p on A ) by INCPROJ:def 10;
consider y being POINT of IPP such that
A5: y on A and
A6: y on L by INCPROJ:def 14;
A7: y in dom (IncProj L,q,R) by A2, A6, Def1;
x9 on K by A1, A3, Def1;
then (IncProj K,p,L) . x = y by A1, A4, A5, A6, Def1;
hence x in dom ((IncProj L,q,R) * (IncProj K,p,L)) by A3, A7, FUNCT_1:21; :: thesis: verum

end;

hence ( x in dom ((IncProj L,q,R) * (IncProj K,p,L)) iff x in dom (IncProj K,p,L) ) by FUNCT_1:21; :: thesis: verum

end;

hence dom ((IncProj L,q,R) * (IncProj K,p,L)) = dom (IncProj K,p,L) by TARSKI:2; :: thesis: rng ((IncProj L,q,R) * (IncProj K,p,L)) = rng (IncProj L,q,R)
for x being set st x in dom (IncProj L,q,R) holds
x in rng (IncProj K,p,L)

proof

let x be set ; :: thesis: ( x in dom (IncProj L,q,R) implies x in rng (IncProj K,p,L) )
assume A8: x in dom (IncProj L,q,R) ; :: thesis: x in rng (IncProj K,p,L)
thus x in rng (IncProj K,p,L) :: thesis: verum

proof

reconsider x9 = x as POINT of IPP by A8;
A9: x9 on L by A2, A8, Def1;
ex y being POINT of IPP st
( y in dom (IncProj K,p,L) & x9 = (IncProj K,p,L) . y )

proof

consider A being LINE of IPP such that
A10: ( x9 on A & p on A ) by INCPROJ:def 10;
consider y being POINT of IPP such that
A11: y on A and
A12: y on K by INCPROJ:def 14;
take y ; :: thesis: ( y in dom (IncProj K,p,L) & x9 = (IncProj K,p,L) . y )
thus y in dom (IncProj K,p,L) by A1, A12, Def1; :: thesis: x9 = (IncProj K,p,L) . y
thus x9 = (IncProj K,p,L) . y by A1, A9, A10, A11, A12, Def1; :: thesis: verum

end;

hence x in rng (IncProj K,p,L) by FUNCT_1:def 5; :: thesis: verum

end;

end;

then dom (IncProj L,q,R) c= rng (IncProj K,p,L) by TARSKI:def 3;
hence rng ((IncProj L,q,R) * (IncProj K,p,L)) = rng (IncProj L,q,R) by RELAT_1:47; :: thesis: verum