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

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