theorem Th21: :: GRAPHSP:21

for F being Element of Funcs ((REAL *),(REAL *))
for f being Element of REAL *
for n, i being Element of NAT holds ((repeat F) . 0) . f = f