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

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] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
(power F_Real) . (r,(n + 1)) = ((power F_Real) . (r,n)) * 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 F_Real) . (r,i) = r |^ i ; :: thesis: verum