let f1, f2 be BinOp of [.0,1.]; :: thesis: ( ( 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)) ; :: thesis: 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 ; :: thesis: ( [x,y] in dom f1 implies f1 . (x,y) = f2 . (x,y) )
assume [x,y] in dom f1 ; :: thesis: 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) ; :: thesis: verum

end;

hence f1 = f2 by A3, BINOP_1:20; :: thesis: verum