theorem :: GRAPHSP:45

for F being Element of Funcs ((REAL *),(REAL *))
for f being Element of REAL *
for n, i being Element of NAT st i < LifeSpan (F,f,n) holds
OuterVx ((((repeat F) . i) . f),n) <> {} by Def4;