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