let k be Integer; :: thesis: ( k <> 0 implies 0 to_power k = 0 )
0 to_power k = 0 #Z k by Def2;
hence ( k <> 0 implies 0 to_power k = 0 ) by PREPOWER:100; :: thesis: verum