let a be Real; :: 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 a to_power n = 0 ; :: thesis: a = 0
then A1: a |^ n = 0 by POWER:41;
assume a <> 0 ; :: thesis: contradiction
hence contradiction by A1, PREPOWER:5; :: thesis: verum