for F, G being Element of Funcs ((REAL *),(REAL *))
for f being Element of REAL *
for i being Nat holds ((repeat (F * G)) . (i + 1)) . f = F . (G . (((repeat (F * G)) . i) . f))