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

per cases ( ( aa = 1 & bb < 1 ) or aa <> 1 or bb >= 1 ) ;

suppose B0: ( aa = 1 & bb < 1 ) ; :: thesis: 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) ; :: thesis: verum

end;

suppose B0: ( aa <> 1 or bb >= 1 ) ; :: thesis: f1 . (a,b) = f2 . (a,b)

( aa <> 1 or bb <= 1 ) by XXREAL_1:1;
then b0: ( aa <> 1 or bb = 1 ) by B0, XXREAL_0:1;
then f1 . (aa,bb) = 1 by A1
.= f2 . (aa,bb) by A2, b0 ;
hence f1 . (a,b) = f2 . (a,b) ; :: thesis: verum

end;

end;

end;

hence f1 = f2 by BINOP_1:def 21; :: thesis: verum