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