let N be 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 Th11
.= (- 1) * ((- 1) * seq) by Th11
.= ((- 1) * (- 1)) * seq by Th13
.= seq by Th16 ; :: thesis: verum