let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s,P holds
0 in dom I
let s be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA st I is_closed_on s,P holds
0 in dom I
let I be Program of SCM+FSA; :: thesis: ( I is_closed_on s,P implies 0 in dom I )
A1: ProgramPart I = I by RELAT_1:209;
reconsider n = IC (Comput ((P +* I),(s +* (Initialize I)),0)) as Element of NAT ;
assume A2: I is_closed_on s,P ; :: thesis: 0 in dom I
then A3: n in dom I by SCMFSA7B:def 7, A1;

per cases ( n = 0 or 0 < n ) ;

suppose n = 0 ; :: thesis: 0 in dom I

hence 0 in dom I by A2, SCMFSA7B:def 7, A1; :: thesis: verum

end;

suppose 0 < n ; :: thesis: 0 in dom I

hence 0 in dom I by A3, AFINSQ_1:def 13; :: thesis: verum

end;

end;