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