let IT be non-zero Complex_Sequence; :: thesis: rng IT c= COMPLEX \ {0c}
not 0c in rng IT by RELAT_1:def 9;
hence rng IT c= COMPLEX \ {0c} by ZFMISC_1:34; :: thesis: verum