let I be Program of SCM+FSA ; :: thesis: for s being State of SCM+FSA st Initialized I c= s holds
IC s = insloc 0
let s be State of SCM+FSA ; :: thesis: ( Initialized I c= s implies IC s = insloc 0 )
assume A1: Initialized I c= s ; :: thesis: IC s = insloc 0
A2: IC (Initialized I) = insloc 0 by SCMFSA6A:25;
IC SCM+FSA in dom (Initialized I) by SCMFSA6A:24;
hence IC s = insloc 0 by A1, A2, AMI_1:97; :: thesis: verum