let a be Int_position; :: thesis: for s being State of SCMPDS holds (Initialize s) . a = s . a
let s be State of SCMPDS; :: thesis: (Initialize s) . a = s . a
not a in dom (Start-At (0,SCMPDS)) by SCMPDS_4:18;
hence (Initialize s) . a = s . a by FUNCT_4:11; :: thesis: verum