let f1, f2 be BinOp of [.0,1.]; ( ( for a, b being Element of [.0,1.] holds f1 . (a,b) = (a * b) / ((a + b) - (a * b)) ) & ( for a, b being Element of [.0,1.] holds f2 . (a,b) = (a * b) / ((a + b) - (a * b)) ) implies f1 = f2 )
assume that
A1:
for a, b being Element of [.0,1.] holds f1 . (a,b) = (a * b) / ((a + b) - (a * b))
and
A2:
for a, b being Element of [.0,1.] holds f2 . (a,b) = (a * b) / ((a + b) - (a * b))
; f1 = f2
for a, b being set st a in [.0,1.] & b in [.0,1.] holds
f1 . (a,b) = f2 . (a,b)
proof
let a,
b be
set ;
( a in [.0,1.] & b in [.0,1.] implies f1 . (a,b) = f2 . (a,b) )
assume
(
a in [.0,1.] &
b in [.0,1.] )
;
f1 . (a,b) = f2 . (a,b)
then reconsider aa =
a,
bb =
b as
Element of
[.0,1.] ;
f1 . (
aa,
bb) =
(aa * bb) / ((aa + bb) - (aa * bb))
by A1
.=
f2 . (
aa,
bb)
by A2
;
hence
f1 . (
a,
b)
= f2 . (
a,
b)
;
verum
end;
hence
f1 = f2
by BINOP_1:def 21; verum