let s be State of SCM+FSA ; :: thesis: Initialize (Initialize s) = Initialize s
( (Initialize s) . (intloc 0 ) = 1 & IC (Initialize s) = insloc 0 ) by SCMFSA6C:3;
hence Initialize (Initialize s) = Initialize s by Th14; :: thesis: verum