let X be RealUnitarySpace; :: thesis: for seq being sequence of X holds (- 1) * seq = - seq
let seq be sequence of X; :: thesis: (- 1) * seq = - seq
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: ((- 1) * seq) . n = (- seq) . n
thus ((- 1) * seq) . n = (- 1) * (seq . n) by NORMSP_1:def 5
.= - (seq . n) by RLVECT_1:16
.= (- seq) . n by Th44 ; :: thesis: verum