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

assume that

A5: for b being bag of X holds p1 . b = (p . b) * a and

A6: for b being bag of X holds p2 . b = (p . b) * a ; :: thesis: p1 = p2

assume that

A5: for b being bag of X holds p1 . b = (p . b) * a and

A6: for b being bag of X holds p2 . b = (p . b) * a ; :: thesis: p1 = p2

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

hence
p1 = p2
; :: thesis: verumlet b be Element of Bags X; :: thesis: p1 . b = p2 . b

reconsider b9 = b as bag of X ;

thus p1 . b = (p . b9) * a by A5

.= p2 . b by A6 ; :: thesis: verum

end;reconsider b9 = b as bag of X ;

thus p1 . b = (p . b9) * a by A5

.= p2 . b by A6 ; :: thesis: verum