let f1, f2 be Function of [:A,A:],REAL; ( ( for a, b being Element of A holds f1 . (a,b) = (G . (a,b)) / (1 + (G . (a,b))) ) & ( for a, b being Element of A holds f2 . (a,b) = (G . (a,b)) / (1 + (G . (a,b))) ) implies f1 = f2 )
assume that
A2:
for a, b being Element of A holds f1 . (a,b) = (G . (a,b)) / (1 + (G . (a,b)))
and
A3:
for a, b being Element of A holds f2 . (a,b) = (G . (a,b)) / (1 + (G . (a,b)))
; f1 = f2
for a, b being Element of A holds f1 . (a,b) = f2 . (a,b)
proof
let a,
b be
Element of
A;
f1 . (a,b) = f2 . (a,b)
f1 . (
a,
b)
= (G . (a,b)) / (1 + (G . (a,b)))
by A2;
hence
f1 . (
a,
b)
= f2 . (
a,
b)
by A3;
verum
end;
hence
f1 = f2
by BINOP_1:2; verum