consider F being Funcs (L,L) -valued sequence such that
A: ( f `^ 1 = F . 1 & F . 0 = id L & ( for i being Nat holds F . (i + 1) = (F . i) * f ) ) by dd;
F . (0 + 1) = (id L) * f by A
.= f ;
hence f `^ 1 = f by A; :: thesis: verum