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