consider f being Function of [:SCM-Instr,(product SCM-OK):],(product SCM-OK) such that
A1: for x being Element of SCM-Instr
for y being SCM-State holds f . (x,y) = SCM-Exec-Res (x,y) from BINOP_1:sch 4();
take curry f ; :: thesis: for x being Element of SCM-Instr
for y being SCM-State holds ((curry f) . x) . y = SCM-Exec-Res (x,y)
let x be Element of SCM-Instr ; :: thesis: for y being SCM-State holds ((curry f) . x) . y = SCM-Exec-Res (x,y)
let y be SCM-State; :: 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