let I be non empty Program of SCM+FSA ; :: thesis: ( 0 in dom (Initialized I) & 0 in dom (I +* (Start-At 0 ,SCM+FSA )) )
A2: 0 in dom I by AFINSQ_1:69;
I c= Initialized I by SCMFSA6A:26;
then dom I c= dom (Initialized I) by RELAT_1:25;
hence 0 in dom (Initialized I) by A2; :: thesis: 0 in dom (I +* (Start-At 0 ,SCM+FSA ))
dom (I +* (Start-At 0 ,SCM+FSA )) = (dom I) \/ (dom (Start-At 0 ,SCM+FSA )) by FUNCT_4:def 1;
hence 0 in dom (I +* (Start-At 0 ,SCM+FSA )) by A2, XBOOLE_0:def 3; :: thesis: verum