deffunc H₃( Element of Funcs A,D1, Element of Funcs A,D2) -> Element of Funcs A,D = f .: $1,$2;
consider b being Function of (Funcs A,D1),(Funcs A,D2),(Funcs A,D) such that
A1: for f1 being Element of Funcs A,D1
for f2 being Element of Funcs A,D2 holds b . f1,f2 = H₃(f1,f2) from BINOP_1:sch 4();
take b ; :: thesis: for f1 being Element of Funcs A,D1
for f2 being Element of Funcs A,D2 holds b . f1,f2 = f .: f1,f2
let f1 be Element of Funcs A,D1; :: thesis: for f2 being Element of Funcs A,D2 holds b . f1,f2 = f .: f1,f2
let f2 be Element of Funcs A,D2; :: thesis: b . f1,f2 = f .: f1,f2
thus b . f1,f2 = f .: f1,f2 by A1; :: thesis: verum