let s be State of SCM+FSA ; :: thesis: for I being initial FinPartState of SCM+FSA st I is_pseudo-closed_on s holds
( I is_pseudo-closed_on s +* (I +* (Start-At 0 ,SCM+FSA )) & pseudo-LifeSpan s,I = pseudo-LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))),I )
let I be initial FinPartState of SCM+FSA ; :: thesis: ( I is_pseudo-closed_on s implies ( I is_pseudo-closed_on s +* (I +* (Start-At 0 ,SCM+FSA )) & pseudo-LifeSpan s,I = pseudo-LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))),I ) )
set s2 = (s +* (I +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ));
A1: (s +* (I +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )) = s +* ((I +* (Start-At 0 ,SCM+FSA )) +* (I +* (Start-At 0 ,SCM+FSA ))) by FUNCT_4:15
.= s +* (I +* (Start-At 0 ,SCM+FSA )) ;
assume A2: I is_pseudo-closed_on s ; :: thesis: ( I is_pseudo-closed_on s +* (I +* (Start-At 0 ,SCM+FSA )) & pseudo-LifeSpan s,I = pseudo-LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))),I )
then A3: for n being Element of NAT st not IC (Comput (ProgramPart ((s +* (I +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),((s +* (I +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),n) in dom I holds
pseudo-LifeSpan s,I <= n by A1, SCMFSA8A:def 5;
A4: for n being Element of NAT st n < pseudo-LifeSpan s,I holds
IC (Comput (ProgramPart ((s +* (I +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),((s +* (I +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),n) in dom I by A2, A1, SCMFSA8A:def 5;
IC (Comput (ProgramPart ((s +* (I +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),((s +* (I +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(pseudo-LifeSpan s,I)) = card (ProgramPart I) by A2, A1, SCMFSA8A:def 5;
hence A5: I is_pseudo-closed_on s +* (I +* (Start-At 0 ,SCM+FSA )) by A4, SCMFSA8A:def 3; :: thesis: pseudo-LifeSpan s,I = pseudo-LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))),I
IC (Comput (ProgramPart ((s +* (I +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),((s +* (I +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(pseudo-LifeSpan s,I)) = card (ProgramPart I) by A2, A1, SCMFSA8A:def 5;
hence pseudo-LifeSpan s,I = pseudo-LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))),I by A3, A5, SCMFSA8A:def 5; :: thesis: verum