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