let f, f' 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
( f' . x,x = 0 & ( x <> y implies f' . x,y = 1 ) ) ) implies f = f' )
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
( f' . x,x = 0 & ( x <> y implies f' . x,y = 1 ) ) ; :: thesis: f = f'

now

let x, y be Element of A; :: thesis: f . x,y = f' . x,y

now

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

suppose A7: x = y ; :: thesis: f . x,y = f' . x,y

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

end;

suppose A8: x <> y ; :: thesis: f . x,y = f' . x,y

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

end;

end;

end;

hence f . x,y = f' . x,y ; :: thesis: verum

end;

hence f = f' by BINOP_1:2; :: thesis: verum