let p, q be Series of n,L; :: thesis: ( ( for x being bag of n holds p . x = - (q . x) ) implies for x being bag of n holds q . x = - (p . x) )
assume A4: for x being bag of n holds p . x = - (q . x) ; :: thesis: for x being bag of n holds q . x = - (p . x)
let x be bag of n; :: thesis: q . x = - (p . x)
thus q . x = - (- (q . x)) by RLVECT_1:30
.= - (p . x) by A4 ; :: thesis: verum