let n be Nat; :: thesis: for x being Element of F_Real st x > 0 holds
(power F_Real) . (x,n) = x to_power n
let x be Element of F_Real; :: thesis: ( x > 0 implies (power F_Real) . (x,n) = x to_power n )
assume A1: x > 0 ; :: thesis: (power F_Real) . (x,n) = x to_power n
defpred S₁[ Nat] means (power F_Real) . (x,$1) = x to_power $1;
(power F_Real) . (x,0) = 1_ F_Real by GROUP_1:def 7
.= 1. F_Real ;
then A2: S₁[ 0 ] by POWER:24;
A3: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A4: S₁[i] ; :: thesis: S₁[i + 1]
set i1 = i + 1;
A5: (power F_Real) . (x,(i + 1)) = ((power F_Real) . (x,i)) * x by GROUP_1:def 7;
x to_power (i + 1) = (x to_power i) * (x to_power 1) by A1, POWER:27;
hence S₁[i + 1] by A4, A5; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A2, A3);
hence (power F_Real) . (x,n) = x to_power n ; :: thesis: verum