set A = [.0,1.];
deffunc H1( Element of [.0,1.], Element of [.0,1.]) -> Element of [.0,1.] = In (1,[.0,1.]);
ex f being Function of [:[.0,1.],[.0,1.]:],[.0,1.] st
for x, y being Element of [.0,1.] holds f . (x,y) = H1(x,y)
from BINOP_1:sch 4();
then consider f being BinOp of [.0,1.] such that
A1:
for x, y being Element of [.0,1.] holds f . (x,y) = H1(x,y)
;
take
f
; for x, y being Element of [.0,1.] holds f . (x,y) = 1
let a, b be Element of [.0,1.]; f . (a,b) = 1
f . (a,b) = H1(a,b)
by A1;
hence
f . (a,b) = 1
by SUBSET_1:def 8, XXREAL_1:1; verum