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

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