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