let n be Nat; :: thesis: for r being Element of F_Real holds power (r,n) = r |^ n
let r be Element of F_Real; :: thesis: power (r,n) = r |^ n
defpred S₁[ Nat] means power (r,$1) = r |^ $1;
power (r,0) = 1_ F_Real by GROUP_1:def 7;
then A1: S₁[ 0 ] by NEWTON:4;

A2: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
power (r,(n + 1)) = (power (r,n1)) * r by GROUP_1:def 7
.= r |^ (n + 1) by A3, NEWTON:6 ;
hence S₁[n + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
hence power (r,n) = r |^ n ; :: thesis: verum