let N be Element of NAT ; :: thesis: for seq being Real_Sequence of N st seq is convergent holds
- seq is convergent
let seq be Real_Sequence of N; :: thesis: ( seq is convergent implies - seq is convergent )
assume seq is convergent ; :: thesis: - seq is convergent
then (- 1) * seq is convergent by Th43;
hence - seq is convergent by Th12; :: thesis: verum