let A be non degenerated commutative Ring; :: thesis: for a being Element of A
for n being Nat st a |^ n in {(0. A)} holds
n <> 0
let a be Element of A; :: thesis: for n being Nat st a |^ n in {(0. A)} holds
n <> 0
let n be Nat; :: thesis: ( a |^ n in {(0. A)} implies n <> 0 )
assume A1: a |^ n in {(0. A)} ; :: thesis: n <> 0
assume n = 0 ; :: thesis: contradiction
then 1_ A in {(0. A)} by A1, BINOM:8;
hence contradiction by TARSKI:def 1; :: thesis: verum