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