let f1, f2 be PartFunc of the Points of IPP,the Points of IPP; :: thesis:
assume that
dom f1 c= the Points of IPP and
A22: for x being POINT of IPP holds
( x in dom f1 iff x on K ) and
A23: for x, y being POINT of IPP st x on K & y on L holds
( f1 . x = y iff ex X being LINE of IPP st
( p on X & x on X & y on X ) ) and
dom f2 c= the Points of IPP and
A24: for x being POINT of IPP holds
( x in dom f2 iff x on K ) and
A25: for x, y being POINT of IPP st x on K & y on L holds
( f2 . x = y iff ex X being LINE of IPP st
( p on X & x on X & y on X ) ) ; :: thesis:
for x being set holds
( x in dom f1 iff x in dom f2 )

let x be set ; :: thesis:
A26: ( x in dom f2 implies x in dom f1 )

assume A27: x in dom f2 ; :: thesis:
then reconsider x = x as Element of the Points of IPP ;
x on K by A24, A27;
hence x in dom f1 by A22; :: thesis:

end;

( x in dom f1 implies x in dom f2 )

assume A28: x in dom f1 ; :: thesis:
then reconsider x = x as Element of the Points of IPP ;
x on K by A22, A28;
hence x in dom f2 by A24; :: thesis:

end;

hence ( x in dom f1 iff x in dom f2 ) by A26; :: thesis:

end;

then A29: dom f1 = dom f2 by TARSKI:2;
for x being POINT of IPP st x in dom f1 holds
f1 . x = f2 . x

let x be POINT of IPP; :: thesis:
consider A2 being LINE of IPP such that
A30: ( p on A2 & x on A2 ) by INCPROJ:def 10;
consider y2 being POINT of IPP such that
A31: ( y2 on A2 & y2 on L ) by INCPROJ:def 14;
assume x in dom f1 ; :: thesis:
then A32: x on K by A22;
then f2 . x = y2 by A25, A30, A31;
hence f1 . x = f2 . x by A23, A32, A30, A31; :: thesis:

end;