deffunc H₁( Subset of R, Subset of R) -> Element of REAL = In ((1 - (JaccardIndex ($1,$2))),REAL);
ex f being Function of [:(bool R),(bool R):],REAL st
for x, y being Element of bool R holds f . (x,y) = H₁(x,y) from BINOP_1:sch 4();
then consider ff being Function of [:(bool R),(bool R):],REAL such that
A1: for x, y being Element of bool R holds ff . (x,y) = H₁(x,y) ;
take ff ; :: thesis: for A, B being Subset of R holds ff . (A,B) = 1 - (JaccardIndex (A,B))
let x, y be Subset of R; :: thesis: ff . (x,y) = 1 - (JaccardIndex (x,y))
ff . (x,y) = In ((1 - (JaccardIndex (x,y))),REAL) by A1
.= 1 - (JaccardIndex (x,y)) ;
hence ff . (x,y) = 1 - (JaccardIndex (x,y)) ; :: thesis: verum