deffunc H₁( Subset of R, Subset of R) -> Element of [.0,1.] = kappa_2 ($1,$2);
ex f being Function of [:(bool the carrier of R),(bool the carrier of R):],[.0,1.] 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 f 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 f . (x,y) = H₁(x,y) ;
take f ; :: thesis: for x, y being Subset of R holds f . (x,y) = kappa_2 (x,y)
thus for x, y being Subset of R holds f . (x,y) = kappa_2 (x,y) by A1; :: thesis: verum