let N be Element of NAT ; :: thesis: for seq being Real_Sequence of N holds - seq = (- 1) * seq
let seq be Real_Sequence of N; :: thesis: - seq = (- 1) * seq

now

let n be Element of NAT ; :: thesis: ((- 1) * seq) . n = (- seq) . n
thus ((- 1) * seq) . n = (- 1) * (seq . n) by Def3
.= - (seq . n) by EUCLID:43
.= (- seq) . n by Def4 ; :: thesis: verum

end;

hence - seq = (- 1) * seq by FUNCT_2:113; :: thesis: verum