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
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: f1 = f2
for x being object holds
( x in dom f1 iff x in dom f2 ) by A24, A22;
then A26: 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 )
consider A2 being LINE of IPP such that
A27: ( p on A2 & x on A2 ) by INCPROJ:def 5;
consider y2 being POINT of IPP such that
A28: ( y2 on A2 & y2 on L ) by INCPROJ:def 9;
assume x in dom f1 ; :: thesis: f1 . x = f2 . x
then A29: x on K by A22;
then f2 . x = y2 by A25, A27, A28;
hence f1 . x = f2 . x by A23, A29, A27, A28; :: thesis: verum

end;

hence f1 = f2 by A26, PARTFUN1:5; :: thesis: verum