for IT being non-zero Complex_Sequence holds rng IT c= COMPLEX \ {0c} by ORDINAL1:def 15, ZFMISC_1:34;