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

( 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)

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

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

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