let seq be Real_Sequence; :: thesis: ( seq is V89() iff - seq is V88() )
- (- seq) = seq ;
hence ( seq is V89() iff - seq is V88() ) ; :: thesis: verum