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

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

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

end;

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