set A = [.0,1.];

deffunc H_{1}( Element of [.0,1.], Element of [.0,1.]) -> Element of [.0,1.] = In ((max ((1 - $1),(min ($1,$2)))),[.0,1.]);

ex f being Function of [:[.0,1.],[.0,1.]:],[.0,1.] st

for x, y being Element of [.0,1.] holds f . (x,y) = H_{1}(x,y)
from BINOP_1:sch 4();

then consider f being BinOp of [.0,1.] such that

A1: for x, y being Element of [.0,1.] holds f . (x,y) = H_{1}(x,y)
;

take f ; :: thesis: for x, y being Element of [.0,1.] holds f . (x,y) = max ((1 - x),(min (x,y)))

let a, b be Element of [.0,1.]; :: thesis: f . (a,b) = max ((1 - a),(min (a,b)))

A2: f . (a,b) = H_{1}(a,b)
by A1;

( max ((1 - a),(min (a,b))) = 1 - a or max ((1 - a),(min (a,b))) = min (a,b) ) by XXREAL_0:16;

hence f . (a,b) = max ((1 - a),(min (a,b))) by A2, SUBSET_1:def 8, FUZNORM1:7, FUZNORM1:1; :: thesis: verum

deffunc H

ex f being Function of [:[.0,1.],[.0,1.]:],[.0,1.] st

for x, y being Element of [.0,1.] holds f . (x,y) = H

then consider f being BinOp of [.0,1.] such that

A1: for x, y being Element of [.0,1.] holds f . (x,y) = H

take f ; :: thesis: for x, y being Element of [.0,1.] holds f . (x,y) = max ((1 - x),(min (x,y)))

let a, b be Element of [.0,1.]; :: thesis: f . (a,b) = max ((1 - a),(min (a,b)))

A2: f . (a,b) = H

( max ((1 - a),(min (a,b))) = 1 - a or max ((1 - a),(min (a,b))) = min (a,b) ) by XXREAL_0:16;

hence f . (a,b) = max ((1 - a),(min (a,b))) by A2, SUBSET_1:def 8, FUZNORM1:7, FUZNORM1:1; :: thesis: verum