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

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