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 SCMFSA6B:4;
I c= Initialized I by SCMFSA6A:26;
hence I +* (Start-At 0 ,SCM+FSA ) c= Initialized I by A1, FUNCT_4:92; :: thesis: verum