deffunc H₁( Subset of R, Subset of R) -> Element of [.0,1.] = In ((1 - (f . ($1,$2))),[.0,1.]);
ex f being preRIF of R st
for x, y being Element of bool the carrier of R holds f . (x,y) = H₁(x,y) from BINOP_1:sch 4();
then consider ff being Function of [:(bool the carrier of R),(bool the carrier of R):],[.0,1.] such that
A1: for x, y being Element of bool the carrier of R holds ff . (x,y) = H₁(x,y) ;
take ff ; :: thesis: for x, y being Subset of R holds ff . (x,y) = 1 - (f . (x,y))
let x, y be Subset of R; :: thesis: ff . (x,y) = 1 - (f . (x,y))
ff . (x,y) = In ((1 - (f . (x,y))),[.0,1.]) by A1
.= 1 - (f . (x,y)) by FUZNORM1:7, SUBSET_1:def 8 ;
hence ff . (x,y) = 1 - (f . (x,y)) ; :: thesis: verum