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