let seq be Complex_Sequence; :: thesis: ( seq is non-zero implies (- seq) " = (- 1r) (#) (seq ") )
(- 1) " = - 1 ;
hence ( seq is non-zero implies (- seq) " = (- 1r) (#) (seq ") ) by Th39; :: thesis: verum