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
A2: IC in dom (Initialize I) by COMPOS_1:141;
A3: ProgramPart I = I by RELAT_1:209;
IC (Comput ((P +* I),(s +* (Initialize I)),0)) = (s +* (Initialize I)) . (IC ) by EXTPRO_1:3
.= IC (Initialize I) by A2, FUNCT_4:14
.= 0 by COMPOS_1:142 ;
hence 0 in dom I by A1, SCMFSA7B:def 7, A3; :: thesis: verum