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