let p be PartState of SCM+FSA; :: thesis: Start-At (0,SCM+FSA) c= Initialized p
Initialized p = Initialize (p +* ((intloc 0) .--> 1)) by FUNCT_4:15;
hence Start-At (0,SCM+FSA) c= Initialized p by FUNCT_4:26; :: thesis: verum