let P be Instruction-Sequence of SCM+FSA; :: thesis: for I being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on s,P holds
0 in dom I
let I be Program of SCM+FSA; :: thesis: for s being State of SCM+FSA st I is_closed_on s,P holds
0 in dom I
let s be State of SCM+FSA; :: thesis: ( I is_closed_on s,P implies 0 in dom I )
assume A1: I is_closed_on s,P ; :: thesis: 0 in dom I
B2: IC in dom (Start-At (0,SCM+FSA)) by MEMSTR_0:15;
IC (Comput ((P +* I),(Initialize s),0)) = (Initialize s) . (IC ) by EXTPRO_1:2
.= IC (Start-At (0,SCM+FSA)) by B2, FUNCT_4:13
.= 0 by FUNCOP_1:72 ;
hence 0 in dom I by A1, SCMFSA7B:def 6; :: thesis: verum