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