let it1, it2 be Series of n,L; :: thesis: ( ( for x being bag of n holds it1 . x = - (p . x) ) & ( for x being bag of n holds it2 . x = - (p . x) ) implies it1 = it2 )
assume that
A2: for x being bag of n holds it1 . x = - (p . x) and
A3: for x being bag of n holds it2 . x = - (p . x) ; :: thesis: it1 = it2

now

let b be Element of Bags n; :: thesis: it1 . b = it2 . b
thus it1 . b = - (p . b) by A2
.= it2 . b by A3 ; :: thesis: verum

end;

hence it1 = it2 by FUNCT_2:113; :: thesis: verum