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