let f1, f2 be BinOp of [.0,1.]; ( ( for x, y being Element of [.0,1.] holds f1 . (x,y) = (1 - x) + (x * y) ) & ( for x, y being Element of [.0,1.] holds f2 . (x,y) = (1 - x) + (x * y) ) implies f1 = f2 )
assume that
A1:
for a, b being Element of [.0,1.] holds f1 . (a,b) = (1 - a) + (a * b)
and
A2:
for a, b being Element of [.0,1.] holds f2 . (a,b) = (1 - a) + (a * b)
; f1 = f2
A3: dom f1 =
[:[.0,1.],[.0,1.]:]
by FUNCT_2:def 1
.=
dom f2
by FUNCT_2:def 1
;
for x, y being object st [x,y] in dom f1 holds
f1 . (x,y) = f2 . (x,y)
proof
let x,
y be
object ;
( [x,y] in dom f1 implies f1 . (x,y) = f2 . (x,y) )
assume
[x,y] in dom f1
;
f1 . (x,y) = f2 . (x,y)
then reconsider xx =
x,
yy =
y as
Element of
[.0,1.] by ZFMISC_1:87;
f1 . (
xx,
yy) =
(1 - xx) + (xx * yy)
by A1
.=
f2 . (
xx,
yy)
by A2
;
hence
f1 . (
x,
y)
= f2 . (
x,
y)
;
verum
end;
hence
f1 = f2
by A3, BINOP_1:20; verum