let f1, f2 be BinOp of [.0,1.]; ( ( for x, y being Element of [.0,1.] holds
( ( y < 1 implies f1 . (x,y) = 0 ) & ( y = 1 implies f1 . (x,y) = 1 ) ) ) & ( for x, y being Element of [.0,1.] holds
( ( y < 1 implies f2 . (x,y) = 0 ) & ( y = 1 implies f2 . (x,y) = 1 ) ) ) implies f1 = f2 )
assume that
A1:
for a, b being Element of [.0,1.] holds
( ( b < 1 implies f1 . (a,b) = 0 ) & ( b = 1 implies f1 . (a,b) = 1 ) )
and
A2:
for a, b being Element of [.0,1.] holds
( ( b < 1 implies f2 . (a,b) = 0 ) & ( b = 1 implies f2 . (a,b) = 1 ) )
; 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.] ;
bb <= 1
by XXREAL_1:1;
per cases then
( bb < 1 or bb = 1 )
by XXREAL_0:1;
suppose B0:
bb < 1
;
f1 . (a,b) = f2 . (a,b)then f1 . (
aa,
bb) =
0
by A1
.=
f2 . (
aa,
bb)
by A2, B0
;
hence
f1 . (
a,
b)
= f2 . (
a,
b)
;
verum end; suppose B1:
bb = 1
;
f1 . (a,b) = f2 . (a,b)then f1 . (
aa,
bb) =
1
by A1
.=
f2 . (
aa,
bb)
by A2, B1
;
hence
f1 . (
a,
b)
= f2 . (
a,
b)
;
verum end; end;
end;
hence
f1 = f2
by BINOP_1:def 21; verum