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 object holds
( x in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) iff x in dom (IncProj (K,p,L)) )

proof

let x be object ; :: 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 5;
consider y being POINT of IPP such that
A5: y on A and
A6: y on L by INCPROJ:def 9;
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:11; :: 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:11; :: 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 object st x in dom (IncProj (L,q,R)) holds
x in rng (IncProj (K,p,L))

proof

let x be object ; :: 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 5;
consider y being POINT of IPP such that
A11: y on A and
A12: y on K by INCPROJ:def 9;
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 3; :: thesis: verum

end;

end;

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