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