let n be Nat; :: thesis: for K being Field
for a being Element of K st a <> 0. K holds
() . (a,n) <> 0. K

let K be Field; :: thesis: for a being Element of K st a <> 0. K holds
() . (a,n) <> 0. K

let a be Element of K; :: thesis: ( a <> 0. K implies () . (a,n) <> 0. K )
defpred S1[ Nat] means for n being Nat st n = \$1 holds
() . (a,n) <> 0. K;
assume A1: a <> 0. K ; :: thesis: () . (a,n) <> 0. K
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume S1[k] ; :: thesis: S1[k + 1]
then A3: (power K) . (a,k) <> 0. K ;
let n be Nat; :: thesis: ( n = k + 1 implies () . (a,n) <> 0. K )
assume n = k + 1 ; :: thesis: () . (a,n) <> 0. K
then (power K) . (a,n) = (() . (a,k)) * a by GROUP_1:def 7;
hence (power K) . (a,n) <> 0. K by ; :: thesis: verum
end;
A4: S1[ 0 ]
proof
A5: 1_ K <> 0. K ;
let n be Nat; :: thesis: ( n = 0 implies () . (a,n) <> 0. K )
assume n = 0 ; :: thesis: () . (a,n) <> 0. K
hence (power K) . (a,n) <> 0. K by ; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A4, A2);
hence (power K) . (a,n) <> 0. K ; :: thesis: verum