let seq be Real_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 Nat such that

A3: (seq ") . n1 = 0 by A2, Th5;

(seq . n1) " = (seq ") . n1 by VALUED_1:10;

hence contradiction by A1, A3, Th5, XCMPLX_1:202; :: thesis: verum

assume that

A1: seq is non-zero and

A2: not seq " is non-zero ; :: thesis: contradiction

consider n1 being Nat such that

A3: (seq ") . n1 = 0 by A2, Th5;

(seq . n1) " = (seq ") . n1 by VALUED_1:10;

hence contradiction by A1, A3, Th5, XCMPLX_1:202; :: thesis: verum