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