let s be Complex_Sequence; :: thesis: ( s is non-zero implies s *' is non-zero )

assume A1: s is non-zero ; :: thesis: s *' is non-zero

assume A1: s is non-zero ; :: thesis: s *' is non-zero

now :: thesis: for n being Element of NAT holds (s *') . n <> 0c

hence
s *' is non-zero
by COMSEQ_1:4; :: thesis: verumlet n be Element of NAT ; :: thesis: (s *') . n <> 0c

s . n <> 0 by A1, COMSEQ_1:3;

then (s . n) *' <> 0c by COMPLEX1:29;

hence (s *') . n <> 0c by Def2; :: thesis: verum

end;s . n <> 0 by A1, COMSEQ_1:3;

then (s . n) *' <> 0c by COMPLEX1:29;

hence (s *') . n <> 0c by Def2; :: thesis: verum