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-VAL R) * SCM-OK)):],(product ((SCM-VAL R) * SCM-OK)) 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 FUNCT_5:69
.= SCM-Exec-Res (x,y) by A1 ; :: thesis: verum