let seq be Complex_Sequence; :: thesis: ( seq is non-zero implies - seq is non-zero )
A1: - (- 1r) = 1r ;
assume seq is non-zero ; :: thesis: - seq is non-zero
hence - seq is non-zero by A1, Th41; :: thesis: verum