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

now

let n be Element of NAT ; :: thesis: (Cseq * (- seq)) . n = ((- Cseq) * seq) . n
thus (Cseq * (- seq)) . n = (Cseq . n) * ((- seq) . n) by Def9
.= (Cseq . n) * (- (seq . n)) by BHSP_1:def 10
.= (- (Cseq . n)) * (seq . n) by CLVECT_1:7
.= ((- Cseq) . n) * (seq . n) by VALUED_1:8
.= ((- Cseq) * seq) . n by Def9 ; :: thesis: verum

end;

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