:: deftheorem Def4 defines LifeSpan GRAPHSP:def 4 :
for f being Element of Funcs ((REAL *),(REAL *))
for g being Element of REAL *
for n being Nat st ex i being Nat st OuterVx ((((repeat f) . i) . g),n) = {} holds
for b₄ being Element of NAT holds
( b₄ = LifeSpan (f,g,n) iff ( OuterVx ((((repeat f) . b₄) . g),n) = {} & ( for k being Nat st OuterVx ((((repeat f) . k) . g),n) = {} holds
b₄ <= k ) ) );