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
now :: thesis: for n being Element of NAT holds (s *') . n <> 0c
let 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;
hence s *' is non-zero by COMSEQ_1:4; :: thesis: verum