let Rseq be Real_Sequence; :: thesis: for X being RealUnitarySpace
for seq being sequence of X holds Rseq * (- seq) = (- Rseq) * seq
let X be RealUnitarySpace; :: thesis: for seq being sequence of X holds Rseq * (- seq) = (- Rseq) * seq
let seq be sequence of X; :: thesis: Rseq * (- seq) = (- Rseq) * seq

now

let n be Element of NAT ; :: thesis: (Rseq * (- seq)) . n = ((- Rseq) * seq) . n
thus (Rseq * (- seq)) . n = (Rseq . n) * ((- seq) . n) by Def9
.= (Rseq . n) * (- (seq . n)) by BHSP_1:def 10
.= (- (Rseq . n)) * (seq . n) by RLVECT_1:38
.= ((- Rseq) . n) * (seq . n) by SEQ_1:14
.= ((- Rseq) * seq) . n by Def9 ; :: thesis: verum

end;

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