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

now

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

end;

hence p1 = p2 by FUNCT_2:113; :: thesis: verum