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
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: (- seq) . n = ((- 1) * seq) . n
thus ((- 1) * seq) . n = (- 1) * (seq . n) by LmDef3
.= - (seq . n) by EUCLID:39
.= (- seq) . n by LmDef4 ; :: thesis: verum