let x be Element of ExtREAL ; :: thesis: for k being Nat holds x |^ (k + 1) = (x |^ k) * x
defpred S₁[ Nat] means x |^ ($1 + 1) = (x |^ $1) * x;
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume x |^ (k + 1) = (x |^ k) * x ; :: thesis: S₁[k + 1]
reconsider k1 = k + 1 as Element of NAT ;
Product ((k1 + 1) |-> x) = Product ((k1 |-> x) ^ <*x*>) by FINSEQ_2:60;
hence S₁[k + 1] by Th8; :: thesis: verum

end;

x |^ (0 + 1) = Product <*x*> by FINSEQ_2:59;
then x |^ (0 + 1) = x by Th7;
then x |^ (0 + 1) = 1. * x by XXREAL_3:81;
then A2: S₁[ 0 ] by Th6, FINSEQ_2:58;
for k being Nat holds S₁[k] from NAT_1:sch 2(A2, A1);
hence for k being Nat holds x |^ (k + 1) = (x |^ k) * x ; :: thesis: verum