deffunc H₁( Subset of R, Subset of R) -> Element of [.0,1.] = In ((((CMap (kappa_1 R)) . ($1,$2)) + ((CMap (kappa_1 R)) . ($2,$1))),[.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) = ((CMap (kappa_1 R)) . (x,y)) + ((CMap (kappa_1 R)) . (y,x))
let x, y be Subset of R; :: thesis: ff . (x,y) = ((CMap (kappa_1 R)) . (x,y)) + ((CMap (kappa_1 R)) . (y,x))
B1: ( 0 <= ((CMap (kappa_1 R)) . (x,y)) + ((CMap (kappa_1 R)) . (y,x)) & ((CMap (kappa_1 R)) . (x,y)) + ((CMap (kappa_1 R)) . (y,x)) <= 1 ) by Prop6e1;
ff . (x,y) = In ((((CMap (kappa_1 R)) . (x,y)) + ((CMap (kappa_1 R)) . (y,x))),[.0,1.]) by A1
.= ((CMap (kappa_1 R)) . (x,y)) + ((CMap (kappa_1 R)) . (y,x)) by B1, XXREAL_1:1, SUBSET_1:def 8 ;
hence ff . (x,y) = ((CMap (kappa_1 R)) . (x,y)) + ((CMap (kappa_1 R)) . (y,x)) ; :: thesis: verum