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 indom 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 indom 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 indom 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 indom 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 indom f1 iff x indom f2 )
byA24, A22; then A26:
dom f1 =dom f2
byTARSKI:2;
for x being POINT of IPP st x indom f1 holds f1 . x = f2 . x