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

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

now

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 by BINOP_1:2; :: thesis: verum