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 (insloc 0 ))) & pseudo-LifeSpan s,I = pseudo-LifeSpan (s +* (I +* (Start-At (insloc 0 )))),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 (insloc 0 ))) & pseudo-LifeSpan s,I = pseudo-LifeSpan (s +* (I +* (Start-At (insloc 0 )))),I ) )
set s2 = (s +* (I +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )));
A1: (s +* (I +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 ))) = s +* ((I +* (Start-At (insloc 0 ))) +* (I +* (Start-At (insloc 0 )))) by FUNCT_4:15
.= s +* (I +* (Start-At (insloc 0 ))) ;
assume A2: I is_pseudo-closed_on s ; :: thesis: ( I is_pseudo-closed_on s +* (I +* (Start-At (insloc 0 ))) & pseudo-LifeSpan s,I = pseudo-LifeSpan (s +* (I +* (Start-At (insloc 0 )))),I )
then A3: for n being Element of NAT st not IC (Computation ((s +* (I +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))),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 (Computation ((s +* (I +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))),n) in dom I by A2, A1, SCMFSA8A:def 5;
IC (Computation ((s +* (I +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))),(pseudo-LifeSpan s,I)) = insloc (card (ProgramPart I)) by A2, A1, SCMFSA8A:def 5;
hence A5: I is_pseudo-closed_on s +* (I +* (Start-At (insloc 0 ))) by A4, SCMFSA8A:def 3; :: thesis: pseudo-LifeSpan s,I = pseudo-LifeSpan (s +* (I +* (Start-At (insloc 0 )))),I
IC (Computation ((s +* (I +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))),(pseudo-LifeSpan s,I)) = insloc (card (ProgramPart I)) by A2, A1, SCMFSA8A:def 5;
hence pseudo-LifeSpan s,I = pseudo-LifeSpan (s +* (I +* (Start-At (insloc 0 )))),I by A3, A5, SCMFSA8A:def 5; :: thesis: verum