consider f being Function of [:SCMPDS-Instr,(product (SCM-VAL * SCM-OK)):],(product (SCM-VAL * SCM-OK)) such that
A1: for x being Element of SCMPDS-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 SCMPDS-Instr
for y being SCM-State holds ((curry f) . x) . y = SCM-Exec-Res (x,y)
let x be Element of SCMPDS-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 FUNCT_5:69
.= SCM-Exec-Res (x,y) by A1 ; :: thesis: verum