let f1, f2 be BinOp of [.0,1.]; ( ( for a, b being Element of [.0,1.] holds f1 . (a,b) = 1 - (t . ((1 - a),(1 - b))) ) & ( for a, b being Element of [.0,1.] holds f2 . (a,b) = 1 - (t . ((1 - a),(1 - b))) ) implies f1 = f2 )
assume that
A1:
for a, b being Element of [.0,1.] holds f1 . (a,b) = 1 - (t . ((1 - a),(1 - b)))
and
A2:
for a, b being Element of [.0,1.] holds f2 . (a,b) = 1 - (t . ((1 - a),(1 - 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
- (t . ((1 - xx),(1 - 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