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

let n be Element of NAT ; :: thesis: (s *' ) . n <> 0c
s . n <> 0c by A1, COMSEQ_1:4;
then (s . n) *' <> 0c by COMPLEX1:114;
hence (s *' ) . n <> 0c by Def2; :: thesis: verum

end;

hence s *' is non-zero by COMSEQ_1:4; :: thesis: verum