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 ;
A4: k in NAT by ORDINAL1:def 13;
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 A4, GROUP_1:def 8;
hence (power K) . (a,n) <> 0. K by A1, A3, VECTSP_1:44; :: thesis: verum

end;

A5: S₁[ 0 ]

proof

A6: 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 A6, GROUP_1:def 8; :: thesis: verum

end;

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