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