deffunc H₁( Element of SCM-Instr R, SCM-State of R) -> SCM-State of R = SCM-Exec-Res $1,$2;
consider f being Function of [:(SCM-Instr R),(product (SCM-OK R)):],(product (SCM-OK R)) such that
A1: for x being Element of SCM-Instr R
for y being SCM-State of R holds f . x,y = H₁(x,y) from BINOP_1:sch 4();
take curry f ; :: thesis: for x being Element of SCM-Instr R
for y being SCM-State of R holds ((curry f) . x) . y = SCM-Exec-Res x,y
let x be Element of SCM-Instr R; :: thesis: for y being SCM-State of R holds ((curry f) . x) . y = SCM-Exec-Res x,y
let y be SCM-State of R; :: thesis: ((curry f) . x) . y = SCM-Exec-Res x,y
thus ((curry f) . x) . y = f . x,y by CAT_2:3
.= SCM-Exec-Res x,y by A1 ; :: thesis: verum