let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X
for k being Nat holds (- seq) ^\ k = - (seq ^\ k)
let seq be sequence of X; :: thesis: for k being Nat holds (- seq) ^\ k = - (seq ^\ k)
let k be Nat; :: thesis: (- seq) ^\ k = - (seq ^\ k)

now :: thesis: for n being Element of NAT holds ((- seq) ^\ k) . n = (- (seq ^\ k)) . n

let n be Element of NAT ; :: thesis: ((- seq) ^\ k) . n = (- (seq ^\ k)) . n
thus ((- seq) ^\ k) . n = (- seq) . (n + k) by NAT_1:def 3
.= - (seq . (n + k)) by BHSP_1:44
.= - ((seq ^\ k) . n) by NAT_1:def 3
.= (- (seq ^\ k)) . n by BHSP_1:44 ; :: thesis: verum

end;

hence (- seq) ^\ k = - (seq ^\ k) by FUNCT_2:63; :: thesis: verum