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

now

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

end;

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