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

now

let n be Element of NAT ; :: thesis: (- (- seq)) . n = seq . n
thus (- (- seq)) . n = - ((- seq) . n) by BHSP_1:def 10
.= - (- (seq . n)) by BHSP_1:def 10
.= seq . n by RLVECT_1:30 ; :: thesis: verum

end;

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