let f1, f2 be BinOp of [.0,1.]; :: thesis: ( ( for a, b being Element of [.0,1.] holds
( ( min (a,b) = 0 implies f1 . (a,b) = max (a,b) ) & ( min (a,b) <> 0 implies f1 . (a,b) = 1 ) ) ) & ( for a, b being Element of [.0,1.] holds
( ( min (a,b) = 0 implies f2 . (a,b) = max (a,b) ) & ( min (a,b) <> 0 implies f2 . (a,b) = 1 ) ) ) implies f1 = f2 )

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