let f1, f2 be PartFunc of the Points of IPP,the Points of IPP; :: thesis: ( dom f1 c= the Points of IPP & ( for x being POINT of IPP holds
( x in dom f1 iff x on K ) ) & ( 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 ) ) ) & dom f2 c= the Points of IPP & ( for x being POINT of IPP holds
( x in dom f2 iff x on K ) ) & ( 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 ) ) ) implies f1 = f2 )
assume that
A18: ( dom f1 c= the Points of IPP & ( for x being POINT of IPP holds
( x in dom f1 iff x on K ) ) ) and
A19: 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
A20: ( dom f2 c= the Points of IPP & ( for x being POINT of IPP holds
( x in dom f2 iff x on K ) ) ) and
A21: 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: f1 = f2
for x being set holds
( x in dom f1 iff x in dom f2 )

proof

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

proof

assume A23: x in dom f1 ; :: thesis: x in dom f2
then reconsider x = x as Element of the Points of IPP ;
x on K by A18, A23;
hence x in dom f2 by A20; :: thesis: verum

end;

( x in dom f2 implies x in dom f1 )

proof

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

end;

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

end;

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

proof

let x be POINT of IPP; :: thesis: ( x in dom f1 implies f1 . x = f2 . x )
assume x in dom f1 ; :: thesis: f1 . x = f2 . x
then A26: x on K by A18;
consider A2 being LINE of IPP such that
A27: ( p on A2 & x on A2 ) by INCPROJ:def 10;
consider y2 being POINT of IPP such that
A28: ( y2 on A2 & y2 on L ) by INCPROJ:def 14;
f2 . x = y2 by A21, A26, A27, A28;
hence f1 . x = f2 . x by A19, A26, A27, A28; :: thesis: verum

end;

hence f1 = f2 by A25, PARTFUN1:34; :: thesis: verum