let R be non empty 1-sorted ; :: thesis: for f being Function of R,R
for n being Nat holds
( f `^ (n + 1) = (f `^ n) * f & (f `^ n) * f = f * (f `^ n) )
let f be Function of R,R; :: thesis: for n being Nat holds
( f `^ (n + 1) = (f `^ n) * f & (f `^ n) * f = f * (f `^ n) )
let n be Nat; :: thesis: ( f `^ (n + 1) = (f `^ n) * f & (f `^ n) * f = f * (f `^ n) )
defpred S1[ Nat] means f `^ ($1 + 1) = (f `^ $1) * f;
IS: now :: thesis: for k being Nat st ( for j being Nat st j < k holds
S1[j] ) holds
S1[k]
let k be Nat; :: thesis: ( ( for j being Nat st j < k holds
S1[j] ) implies S1[k] )
assume AS: for j being Nat st j < k holds
S1[j] ; :: thesis: S1[k]
consider F being Funcs (R,R) -valued sequence such that
A: ( f `^ (k + 1) = F . (k + 1) & F . 0 = id R & ( for i being Nat holds F . (i + 1) = (F . i) * f ) ) by dd;
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
B: for m being Element of NAT st m <= k holds
F . m = f `^ m
proof
let m be Element of NAT ; :: thesis: ( m <= k implies F . m = f `^ m )
assume C: m <= k ; :: thesis: F . m = f `^ m
defpred S2[ Nat] means F . $1 = f `^ $1;
IA: S2[ 0 ] by A, T1;
IS: now :: thesis: for j being Element of NAT st 0 <= j & j < k1 & S2[j] holds
S2[j + 1]
let j be Element of NAT ; :: thesis: ( 0 <= j & j < k1 & S2[j] implies S2[j + 1] )
assume E: ( 0 <= j & j < k1 ) ; :: thesis: ( S2[j] implies S2[j + 1] )
assume IV: S2[j] ; :: thesis: S2[j + 1]
F . (j + 1) = (f `^ j) * f by A, IV
.= f `^ (j + 1) by E, AS ;
hence S2[j + 1] ; :: thesis: verum
end;
for j being Element of NAT st 0 <= j & j <= k1 holds
S2[j] from INT_1:sch 7(IA, IS);
 hence F . m = f `^ m by C; :: thesis: verum
end;
f `^ (k + 1) = (F . k) * f by A
.= (f `^ k1) * f by B ;
hence S1[k] ; :: thesis: verum
end;
I: for k being Nat holds S1[k] from NAT_1:sch 4(IS);
 hence f `^ (n + 1) = (f `^ n) * f ; :: thesis: (f `^ n) * f = f * (f `^ n)
defpred S2[ Nat] means (f `^ $1) * f = f * (f `^ $1);
(f `^ 0) * f = (id R) * f by T1
.= f * (id R)
.= f * (f `^ 0) by T1 ;
then IA: S2[ 0 ] ;
IS: now :: thesis: for k being Nat st S2[k] holds
S2[k + 1]
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume IV: S2[k] ; :: thesis: S2[k + 1]
(f `^ (k + 1)) * f = (f * (f `^ k)) * f by I, IV
.= f * ((f `^ k) * f) by T2
.= f * (f `^ (k + 1)) by I ;
hence S2[k + 1] ; :: thesis: verum
end;
for k being Nat holds S2[k] from NAT_1:sch 2(IA, IS);
 hence (f `^ n) * f = f * (f `^ n) ; :: thesis: verum