let s be State of ; :: thesis: for I being Program of st Initialized I c= s holds
IC s = inspos 0
let I be Program of ; :: thesis: ( Initialized I c= s implies IC s = inspos 0 )
A1: IC (Initialized I) = inspos 0 by SCMPDS_4:8;
A2: IC SCMPDS in dom (Initialized I) by SCMPDS_4:7;
assume Initialized I c= s ; :: thesis: IC s = inspos 0
hence IC s = inspos 0 by A1, A2, AMI_1:97; :: thesis: verum