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 COMPOS_1:141;
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 EXTPRO_1:3
.= IC (I +* (Start-At (0,SCM+FSA))) by A2, FUNCT_4:14
.= 0 by COMPOS_1:142 ;
hence 0 in dom I by A1, SCMFSA7B:def 7; :: thesis: verum