let f, f9 be Function of [:A,A:],REAL; :: thesis: ( ( for x, y being Element of A holds
( f . (x,x) = 0 & ( x <> y implies f . (x,y) = 1 ) ) ) & ( for x, y being Element of A holds
( f9 . (x,x) = 0 & ( x <> y implies f9 . (x,y) = 1 ) ) ) implies f = f9 )
assume that
A5: for x, y being Element of A holds
( f . (x,x) = 0 & ( x <> y implies f . (x,y) = 1 ) ) and
A6: for x, y being Element of A holds
( f9 . (x,x) = 0 & ( x <> y implies f9 . (x,y) = 1 ) ) ; :: thesis: f = f9

now :: thesis: for x, y being Element of A holds f . (x,y) = f9 . (x,y)

let x, y be Element of A; :: thesis: f . (x,y) = f9 . (x,y)

now :: thesis: f . (x,y) = f9 . (x,y)

per cases ( x = y or x <> y ) ;

suppose A7: x = y ; :: thesis: f . (x,y) = f9 . (x,y)

hence f . (x,y) = 0 by A5
.= f9 . (x,y) by A6, A7 ;
:: thesis: verum

end;

suppose A8: x <> y ; :: thesis: f . (x,y) = f9 . (x,y)

hence f . (x,y) = 1 by A5
.= f9 . (x,y) by A6, A8 ;
:: thesis: verum

end;

end;

end;

hence f . (x,y) = f9 . (x,y) ; :: thesis: verum

end;

hence f = f9 ; :: thesis: verum