for seq being Complex_Sequence holds
( seq is non-zero iff for n being Element of NAT holds seq . n <> 0c )