:: deftheorem Def5 defines while_do GRAPHSP:def 5 :
for f being Element of Funcs ((REAL *),(REAL *))
for n being Nat
for b₃ being Element of Funcs ((REAL *),(REAL *)) holds
( b₃ = while_do (f,n) iff ( dom b₃ = REAL * & ( for h being Element of REAL * holds b₃ . h = ((repeat f) . (LifeSpan (f,h,n))) . h ) ) );