let F, G be Element of Funcs ((REAL *),(REAL *)); :: thesis: for f being Element of REAL *
for i being Nat holds ((repeat (F * G)) . (i + 1)) . f = F . (G . (((repeat (F * G)) . i) . f))
let f be Element of REAL * ; :: thesis: for i being Nat holds ((repeat (F * G)) . (i + 1)) . f = F . (G . (((repeat (F * G)) . i) . f))
let i be Nat; :: thesis: ((repeat (F * G)) . (i + 1)) . f = F . (G . (((repeat (F * G)) . i) . f))
set Fi = (repeat (F * G)) . i;
set ff = ((repeat (F * G)) . i) . f;
set FFi = (F * G) * ((repeat (F * G)) . i);
A1: dom (F * G) = REAL * by Lm5;
A2: dom ((F * G) * ((repeat (F * G)) . i)) = REAL * by Lm5;
thus ((repeat (F * G)) . (i + 1)) . f = ((F * G) * ((repeat (F * G)) . i)) . f by Def2
.= (F * G) . (((repeat (F * G)) . i) . f) by A2, FUNCT_1:12
.= F . (G . (((repeat (F * G)) . i) . f)) by A1, FUNCT_1:12 ; :: thesis: verum