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 :: thesis: for n being Element of NAT holds (Cseq * (- seq)) . n = ((- Cseq) * seq) . n

let n be Element of NAT ; :: thesis: (Cseq * (- seq)) . n = ((- Cseq) * seq) . n
thus (Cseq * (- seq)) . n = (Cseq . n) * ((- seq) . n) by Def8
.= (Cseq . n) * (- (seq . n)) by BHSP_1:44
.= (- (Cseq . n)) * (seq . n) by CLVECT_1:6
.= ((- Cseq) . n) * (seq . n) by VALUED_1:8
.= ((- Cseq) * seq) . n by Def8 ; :: thesis: verum

end;

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