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
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: K13((Rseq * (- seq)),n) = K13(((- Rseq) * seq),n)
thus (Rseq * (- seq)) . n = (Rseq . n) * ((- seq) . n) by Def9
.= (Rseq . n) * (- (seq . n)) by BHSP_1:44
.= (- (Rseq . n)) * (seq . n) by RLVECT_1:24
.= ((- Rseq) . n) * (seq . n) by SEQ_1:10
.= ((- Rseq) * seq) . n by Def9 ; :: thesis: verum