let N be Element of NAT ; :: thesis: for seq being Real_Sequence of N holds - (- seq) = seq
let seq be Real_Sequence of N; :: thesis: - (- seq) = seq
thus - (- seq) = (- 1) * (- seq) by Th12
.= (- 1) * ((- 1) * seq) by Th12
.= ((- 1) * (- 1)) * seq by Th14
.= seq by Th17 ; :: thesis: verum