let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: 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 COMPOS_1:52;
IC (Comput ((P +* I),(Initialize s),0)) = (Initialize s) . (IC ) by EXTPRO_1:3
.= IC (Start-At (0,SCM+FSA)) by B2, FUNCT_4:14
.= 0 by COMPOS_1:64 ;
hence 0 in dom I by A1, SCMFSA7B:def 7; :: thesis: verum