let f1, f2 be Function of [:A,A:],REAL; :: thesis: ( ( 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))) ; :: thesis: f1 = f2
for a, b being Element of A holds f1 . (a,b) = f2 . (a,b)

proof

let a, b be Element of A; :: thesis: 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; :: thesis: verum

end;

hence f1 = f2 by BINOP_1:2; :: thesis: verum