set I = <%i%>;
A1: ProgramPart <%i%> = <%i%> by RELAT_1:209;
let s be State of SCM+FSA; :: according to SCMFSA8A:def 4 :: thesis: for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds <%i%> is_pseudo-closed_on s,P
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: <%i%> is_pseudo-closed_on s,P
set s1 = s +* (Initialize <%i%>);
dom <%i%> = 1 by AFINSQ_1:36;
then A2: 0 in dom <%i%> by CARD_1:87, TARSKI:def 1;
dom (P +* <%i%>) = (dom P) \/ (dom <%i%>) by FUNCT_4:def 1;
then A3: 0 in dom (P +* <%i%>) by A2, XBOOLE_0:def 3;
A4: CurInstr ((P +* <%i%>),(s +* (Initialize <%i%>))) = (P +* <%i%>) /. 0 by COMPOS_1:def 16
.= (P +* <%i%>) . 0 by A3, PARTFUN1:def 8
.= <%i%> . 0 by A2, FUNCT_4:14
.= i by AFINSQ_1:38 ;
take 1 ; :: according to SCMFSA8A:def 3 :: thesis: ( IC (Comput ((P +* (ProgramPart <%i%>)),(s +* (Initialize <%i%>)),1)) = card (ProgramPart <%i%>) & ( for n being Element of NAT st n < 1 holds
IC (Comput ((P +* (ProgramPart <%i%>)),(s +* (Initialize <%i%>)),n)) in dom <%i%> ) )
thus IC (Comput ((P +* (ProgramPart <%i%>)),(s +* (Initialize <%i%>)),1)) = IC (Comput ((P +* <%i%>),(s +* (Initialize <%i%>)),(0 + 1))) by A1
.= IC (Following ((P +* <%i%>),(Comput ((P +* <%i%>),(s +* (Initialize <%i%>)),0)))) by EXTPRO_1:4
.= IC (Following ((P +* <%i%>),(s +* (Initialize <%i%>)))) by EXTPRO_1:3
.= succ (IC (s +* (Initialize <%i%>))) by A4, AMISTD_1:def 16
.= succ 0 by COMPOS_1:def 16
.= card <%i%> by AFINSQ_1:38
.= card (ProgramPart <%i%>) by RELAT_1:209 ; :: thesis: for n being Element of NAT st n < 1 holds
IC (Comput ((P +* (ProgramPart <%i%>)),(s +* (Initialize <%i%>)),n)) in dom <%i%>
let n be Element of NAT ; :: thesis: ( n < 1 implies IC (Comput ((P +* (ProgramPart <%i%>)),(s +* (Initialize <%i%>)),n)) in dom <%i%> )
assume n < 1 ; :: thesis: IC (Comput ((P +* (ProgramPart <%i%>)),(s +* (Initialize <%i%>)),n)) in dom <%i%>
then n = 0 by NAT_1:14;
then A5: IC (Comput ((P +* <%i%>),(s +* (Initialize <%i%>)),n)) = IC (s +* (Initialize <%i%>)) by EXTPRO_1:3
.= 0 by COMPOS_1:def 16 ;
dom <%i%> = 1 by AFINSQ_1:36;
hence IC (Comput ((P +* (ProgramPart <%i%>)),(s +* (Initialize <%i%>)),n)) in dom <%i%> by A5, CARD_1:87, TARSKI:def 1, A1; :: thesis: verum