let p1, p2 be Series of X,L; :: thesis: ( ( for b being bag of X holds p1 . b = a * (p . b) ) & ( for b being bag of X holds p2 . b = a * (p . b) ) implies p1 = p2 )
assume that
A2: for b being bag of X holds p1 . b = a * (p . b) and
A3: for b being bag of X holds p2 . b = a * (p . b) ; :: thesis: p1 = p2

now :: thesis: for b being Element of Bags X holds p1 . b = p2 . b

let b be Element of Bags X; :: thesis: p1 . b = p2 . b
reconsider b9 = b as bag of X ;
thus p1 . b = a * (p . b9) by A2
.= p2 . b by A3 ; :: thesis: verum

end;

hence p1 = p2 ; :: thesis: verum