set P = <%i%>;
let s be State of SCM+FSA; :: according to SCMFSA8A:def 4 :: thesis: <%i%> is_pseudo-closed_on s
set s1 = s +* (<%i%> +* (Start-At (0,SCM+FSA)));
dom <%i%> = 1 by AFINSQ_1:36;
then F: 0 in dom <%i%> by CARD_1:87, TARSKI:def 1;
s +* (<%i%> +* (Start-At (0,SCM+FSA))) = Initialize (s +* <%i%>) by FUNCT_4:15;
then E: ProgramPart (s +* (<%i%> +* (Start-At (0,SCM+FSA)))) = (ProgramPart (s +* <%i%>)) +* (ProgramPart (Start-At (0,SCM+FSA))) by FUNCT_4:75
.= (ProgramPart (s +* <%i%>)) +* {} by COMPOS_1:27
.= ProgramPart (s +* <%i%>) by FUNCT_4:22
.= (ProgramPart s) +* (ProgramPart <%i%>) by FUNCT_4:75
.= (ProgramPart s) +* <%i%> by RELAT_1:209 ;
dom ((ProgramPart s) +* <%i%>) = (dom (ProgramPart s)) \/ (dom <%i%>) by FUNCT_4:def 1;
then G: 0 in dom ((ProgramPart s) +* <%i%>) by F, XBOOLE_0:def 3;
D: IC (s +* (<%i%> +* (Start-At (0,SCM+FSA)))) = 0 by COMPOS_1:def 16;
then C: CurInstr ((ProgramPart (s +* (<%i%> +* (Start-At (0,SCM+FSA))))),(s +* (<%i%> +* (Start-At (0,SCM+FSA))))) = (ProgramPart (s +* (<%i%> +* (Start-At (0,SCM+FSA))))) /. 0
.= (ProgramPart (s +* (<%i%> +* (Start-At (0,SCM+FSA))))) . 0 by G, E, PARTFUN1:def 8
.= ((ProgramPart s) +* <%i%>) . 0 by E
.= <%i%> . 0 by F, FUNCT_4:14
.= i by AFINSQ_1:38 ;
take 1 ; :: according to SCMFSA8A:def 3 :: thesis: ( IC (Comput ((ProgramPart (s +* (<%i%> +* (Start-At (0,SCM+FSA))))),(s +* (<%i%> +* (Start-At (0,SCM+FSA)))),1)) = card (ProgramPart <%i%>) & ( for n being Element of NAT st n < 1 holds
IC (Comput ((ProgramPart (s +* (<%i%> +* (Start-At (0,SCM+FSA))))),(s +* (<%i%> +* (Start-At (0,SCM+FSA)))),n)) in dom <%i%> ) )
thus IC (Comput ((ProgramPart (s +* (<%i%> +* (Start-At (0,SCM+FSA))))),(s +* (<%i%> +* (Start-At (0,SCM+FSA)))),1)) = IC (Comput ((ProgramPart (s +* (<%i%> +* (Start-At (0,SCM+FSA))))),(s +* (<%i%> +* (Start-At (0,SCM+FSA)))),(0 + 1)))
.= IC (Following ((ProgramPart (s +* (<%i%> +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* (<%i%> +* (Start-At (0,SCM+FSA))))),(s +* (<%i%> +* (Start-At (0,SCM+FSA)))),0)))) by EXTPRO_1:4
.= IC (Following ((ProgramPart (s +* (<%i%> +* (Start-At (0,SCM+FSA))))),(s +* (<%i%> +* (Start-At (0,SCM+FSA)))))) by EXTPRO_1:3
.= IC (Exec ((CurInstr ((ProgramPart (s +* (<%i%> +* (Start-At (0,SCM+FSA))))),(s +* (<%i%> +* (Start-At (0,SCM+FSA)))))),(s +* (<%i%> +* (Start-At (0,SCM+FSA))))))
.= IC (Exec (i,(s +* (<%i%> +* (Start-At (0,SCM+FSA)))))) by C
.= succ (IC (s +* (<%i%> +* (Start-At (0,SCM+FSA))))) by AMISTD_1:def 16
.= succ 0 by D
.= 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 ((ProgramPart (s +* (<%i%> +* (Start-At (0,SCM+FSA))))),(s +* (<%i%> +* (Start-At (0,SCM+FSA)))),n)) in dom <%i%>
let n be Element of NAT ; :: thesis: ( n < 1 implies IC (Comput ((ProgramPart (s +* (<%i%> +* (Start-At (0,SCM+FSA))))),(s +* (<%i%> +* (Start-At (0,SCM+FSA)))),n)) in dom <%i%> )
assume n < 1 ; :: thesis: IC (Comput ((ProgramPart (s +* (<%i%> +* (Start-At (0,SCM+FSA))))),(s +* (<%i%> +* (Start-At (0,SCM+FSA)))),n)) in dom <%i%>
then n = 0 by NAT_1:14;
then A: IC (Comput ((ProgramPart (s +* (<%i%> +* (Start-At (0,SCM+FSA))))),(s +* (<%i%> +* (Start-At (0,SCM+FSA)))),n)) = IC (s +* (<%i%> +* (Start-At (0,SCM+FSA)))) by EXTPRO_1:3
.= 0 by D ;
dom <%i%> = 1 by AFINSQ_1:36;
hence IC (Comput ((ProgramPart (s +* (<%i%> +* (Start-At (0,SCM+FSA))))),(s +* (<%i%> +* (Start-At (0,SCM+FSA)))),n)) in dom <%i%> by A, CARD_1:87, TARSKI:def 1; :: thesis: verum