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 Th43; :: thesis: verum