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