let n be Nat; :: thesis: for K being Field
for a1 being Element of K st a1 = 0. K & n > 1 holds
a1 |^ n = 0. K
let K be Field; :: thesis: for a1 being Element of K st a1 = 0. K & n > 1 holds
a1 |^ n = 0. K
let a1 be Element of K; :: thesis: ( a1 = 0. K & n > 1 implies a1 |^ n = 0. K )
assume A1: a1 = 0. K ; :: thesis: ( not n > 1 or a1 |^ n = 0. K )
assume A2: n > 1 ; :: thesis: a1 |^ n = 0. K
n - 1 is Nat by A2, NAT_1:20;
then consider n1 being Nat such that
A3: n1 = n - 1 ;
a1 |^ n = a1 |^ (n1 + 1) by A3
.= (a1 |^ n1) * a1 by EC_PF_1:24 ;
hence a1 |^ n = 0. K by A1; :: thesis: verum