deffunc H1( 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) = H1(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) = H1(x,y)
;
take
ff
; for x, y being Subset of R holds ff . (x,y) = 1 - (f . (x,y))
let x, y be Subset of R; 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))
; verum