let I be non empty Program of SCM+FSA ; :: thesis: ( 0 in dom I & 0 in dom (Initialized I) & 0 in dom (I +* (Start-At 0 ,SCM+FSA )) )
consider iloc being set such that
A1: iloc in dom I by XBOOLE_0:def 1;
dom I c= NAT by RELAT_1:def 18;
then reconsider iloc = iloc as Element of NAT by A1;
reconsider i = iloc as Element of NAT ;
( 0 < i or 0 = i ) ;
hence A2: 0 in dom I by A1, SCMNORM:def 1; :: thesis: ( 0 in dom (Initialized I) & 0 in dom (I +* (Start-At 0 ,SCM+FSA )) )
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