let X be RealUnitarySpace; :: thesis: for seq being sequence of X holds seq = - (- seq)
let seq be sequence of X; :: thesis: seq = - (- seq)
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: seq . n = (- (- seq)) . n
thus (- (- seq)) . n = - ((- seq) . n) by Th44
.= - (- (seq . n)) by Th44
.= seq . n by RLVECT_1:17 ; :: thesis: verum