let a be real number ; :: thesis: for n being Element of NAT st a to_power n = 0 holds
a = 0
let n be Element of NAT ; :: thesis: ( a to_power n = 0 implies a = 0 )
assume A1: a to_power n = 0 ; :: thesis: a = 0
assume A2: a <> 0 ; :: thesis: contradiction
a |^ n = 0 by A1, POWER:46;
hence contradiction by A2, PREPOWER:12; :: thesis: verum