let seq be Complex_Sequence; :: thesis: ( seq is non-zero implies seq " is non-zero )
assume that
A1: seq is non-zero and
A2: not seq " is non-zero ; :: thesis: contradiction
consider n1 being Element of NAT such that
A3: (seq ") . n1 = 0c by A2, Th4;
(seq . n1) " = (seq ") . n1 by VALUED_1:10;
hence contradiction by A1, A3, Th4, XCMPLX_1:202; :: thesis: verum