let CNS be ComplexNormSpace; :: thesis: for seq being sequence of CNS holds - seq = (- 1r) * seq
let seq be sequence of CNS; :: thesis: - seq = (- 1r) * seq

now :: thesis: for n being Element of NAT holds ((- 1r) * seq) . n = (- seq) . n

let n be Element of NAT ; :: thesis: ((- 1r) * seq) . n = (- seq) . n
thus ((- 1r) * seq) . n = (- 1r) * (seq . n) by CLVECT_1:def 14
.= - (seq . n) by CLVECT_1:3
.= (- seq) . n by BHSP_1:44 ; :: thesis: verum

end;

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