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

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