let hh be Real_Sequence; :: thesis: ( hh = h ^\ n implies hh is non-zero )
assume A1: hh = h ^\ n ; :: thesis: hh is non-zero
rng hh c= rng h by A1, NAT_1:55;
hence not 0 in rng hh ; :: according to ORDINAL1:def 15 :: thesis: verum