let s be State of SCM+FSA; :: thesis: for P being initial FinPartState of SCM+FSA st P is_pseudo-closed_on s holds
for k being Element of NAT st ( for n being Element of NAT st n <= k holds
IC (Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),n)) in dom P ) holds
k < pseudo-LifeSpan (s,P)
let P be initial FinPartState of SCM+FSA; :: thesis: ( P is_pseudo-closed_on s implies for k being Element of NAT st ( for n being Element of NAT st n <= k holds
IC (Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),n)) in dom P ) holds
k < pseudo-LifeSpan (s,P) )
assume P is_pseudo-closed_on s ; :: thesis: for k being Element of NAT st ( for n being Element of NAT st n <= k holds
IC (Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),n)) in dom P ) holds
k < pseudo-LifeSpan (s,P)
then IC (Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),(pseudo-LifeSpan (s,P)))) = card (ProgramPart P) by SCMFSA8A:def 5;
then A1: not IC (Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),(pseudo-LifeSpan (s,P)))) in dom (ProgramPart P) ;
let k be Element of NAT ; :: thesis: ( ( for n being Element of NAT st n <= k holds
IC (Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),n)) in dom P ) implies k < pseudo-LifeSpan (s,P) )
assume A2: for n being Element of NAT st n <= k holds
IC (Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),n)) in dom P ; :: thesis: k < pseudo-LifeSpan (s,P)
assume pseudo-LifeSpan (s,P) <= k ; :: thesis: contradiction
hence contradiction by A2, A1, COMPOS_1:16; :: thesis: verum