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 ) )
assume A1: 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 )
set s2 = (s +* (I +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )));
A2: (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 ))) ;
then A3: ( IC (Computation ((s +* (I +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))),(pseudo-LifeSpan s,I)) = insloc (card (ProgramPart I)) & ( 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;
( IC (Computation ((s +* (I +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 )))),(pseudo-LifeSpan s,I)) = insloc (card (ProgramPart I)) & ( 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 A1, A2, SCMFSA8A:def 5;
hence I is_pseudo-closed_on s +* (I +* (Start-At (insloc 0 ))) by SCMFSA8A:def 3; :: thesis: pseudo-LifeSpan s,I = pseudo-LifeSpan (s +* (I +* (Start-At (insloc 0 )))),I
hence pseudo-LifeSpan s,I = pseudo-LifeSpan (s +* (I +* (Start-At (insloc 0 )))),I by A3, SCMFSA8A:def 5; :: thesis: verum