let R be non empty 1-sorted ; :: thesis: for f being Function of R,R holds
( f `^ 0 = id R & f `^ 1 = f & f `^ 2 = f * f )
let f be Function of R,R; :: thesis: ( f `^ 0 = id R & f `^ 1 = f & f `^ 2 = f * f )
consider F being Funcs (R,R) -valued sequence such that
A: ( f `^ 0 = F . 0 & F . 0 = id R & ( for i being Nat holds F . (i + 1) = (F . i) * f ) ) by dd;
thus f `^ 0 = id R by A; :: thesis: ( f `^ 1 = f & f `^ 2 = f * f )
thus f `^ 1 = f ; :: thesis: f `^ 2 = f * f
consider F being Funcs (R,R) -valued sequence such that
A: ( f `^ 2 = F . 2 & F . 0 = id R & ( for i being Nat holds F . (i + 1) = (F . i) * f ) ) by dd;
F . (0 + 1) = (id R) * f by A
.= f ;
then F . (1 + 1) = f * f by A;
hence f `^ 2 = f * f by A; :: thesis: verum