let I be Program of SCM+FSA; :: thesis: Initialize I c= Initialized I
Initialized I = Initialize (I +* ((intloc 0) .--> 1)) by FUNCT_4:15;
then A1: Start-At (0,SCM+FSA) c= Initialized I by FUNCT_4:26;
I c= Initialized I by SCMFSA6A:26;
hence Initialize I c= Initialized I by A1, FUNCT_4:92; :: thesis: verum