let I be Program of SCM+FSA ; :: thesis: I +* (Start-At 0 ,SCM+FSA ) c= Initialized I
set SA = Start-At 0 ,SCM+FSA ;
( Start-At 0 ,SCM+FSA c= Initialized I & I c= Initialized I ) by FUNCT_4:26, SCMFSA6A:26;
then A1: I \/ (Start-At 0 ,SCM+FSA ) c= Initialized I by XBOOLE_1:8;
I +* (Start-At 0 ,SCM+FSA ) c= I \/ (Start-At 0 ,SCM+FSA ) by FUNCT_4:30;
hence I +* (Start-At 0 ,SCM+FSA ) c= Initialized I by A1, XBOOLE_1:1; :: thesis: verum