let n be Nat; :: thesis: for K being Field
for a being Element of K st a <> 0. K holds
(power K) . (a,n) <> 0. K
let K be Field; :: thesis: for a being Element of K st a <> 0. K holds
(power K) . (a,n) <> 0. K
let a be Element of K; :: thesis: ( a <> 0. K implies (power K) . (a,n) <> 0. K )
defpred S₁[ Nat] means for n being Nat st n = $1 holds
(power K) . (a,n) <> 0. K;
assume A1: a <> 0. K ; :: thesis: (power K) . (a,n) <> 0. K
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
then A3: (power K) . (a,k) <> 0. K ;
let n be Nat; :: thesis: ( n = k + 1 implies (power K) . (a,n) <> 0. K )
assume n = k + 1 ; :: thesis: (power K) . (a,n) <> 0. K
then (power K) . (a,n) = ((power K) . (a,k)) * a by GROUP_1:def 7;
hence (power K) . (a,n) <> 0. K by A1, A3, VECTSP_1:12; :: thesis: verum

end;

A4: S₁[ 0 ]

proof

A5: 1_ K <> 0. K ;
let n be Nat; :: thesis: ( n = 0 implies (power K) . (a,n) <> 0. K )
assume n = 0 ; :: thesis: (power K) . (a,n) <> 0. K
hence (power K) . (a,n) <> 0. K by A5, GROUP_1:def 7; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A4, A2);
hence (power K) . (a,n) <> 0. K ; :: thesis: verum