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