let n be Nat; :: thesis: for x being Element of F_Real st x <> 0. F_Real holds
(power F_Real) . (x,n) <> 0. F_Real
let x be Element of F_Real; :: thesis: ( x <> 0. F_Real implies (power F_Real) . (x,n) <> 0. F_Real )
assume A1: x <> 0. F_Real ; :: thesis: (power F_Real) . (x,n) <> 0. F_Real
defpred S₁[ Nat] means (power F_Real) . (x,$1) <> 0. F_Real;
(power F_Real) . (x,0) = 1_ F_Real by GROUP_1:def 7;
then A2: S₁[ 0 ] ;
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;
(power F_Real) . (x,(i + 1)) = ((power F_Real) . (x,i)) * x by GROUP_1:def 7;
hence S₁[i + 1] by A1, A4; :: thesis: verum

end;

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