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 ( Start-At (0,SCM+FSA) c= Initialized I & I c= Initialized I ) by FUNCT_4:26, Th26;
then A1: I \/ (Start-At (0,SCM+FSA)) c= Initialized I by XBOOLE_1:8;
Initialize I c= I \/ (Start-At (0,SCM+FSA)) by FUNCT_4:30;
hence Initialize I c= Initialized I by A1, XBOOLE_1:1; :: thesis: verum