let I be Program of SCM+FSA ; :: thesis: for s being State of SCM+FSA st I is_closed_on s holds
0 in dom I
let s be State of SCM+FSA ; :: thesis: ( I is_closed_on s implies 0 in dom I )
assume A1: I is_closed_on s ; :: thesis: 0 in dom I
A2: IC SCM+FSA in dom (I +* (Start-At 0 ,SCM+FSA )) by SF_MASTR:65;
IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),0 ) = (s +* (I +* (Start-At 0 ,SCM+FSA ))) . (IC SCM+FSA ) by AMI_1:13
.= (I +* (Start-At 0 ,SCM+FSA )) . (IC SCM+FSA ) by A2, FUNCT_4:14
.= 0 by SF_MASTR:66 ;
hence 0 in dom I by A1, SCMFSA7B:def 7; :: thesis: verum