let S1, S2 be Series of m,L; :: thesis: ( ( for b being bag of m holds S1 . b = P . ((2 (#) b) +* (0,(b . 0))) ) & ( for b being bag of m holds S2 . b = P . ((2 (#) b) +* (0,(b . 0))) ) implies S1 = S2 )
assume that
A3: for b being bag of m holds S1 . b = P . ((2 (#) b) +* (0,(b . 0))) and
A4: for b being bag of m holds S2 . b = P . ((2 (#) b) +* (0,(b . 0))) ; :: thesis: S1 = S2
for x being object st x in Bags m holds
S1 . x = S2 . x

proof

let b be object ; :: thesis: ( b in Bags m implies S1 . b = S2 . b )
assume A5: b in Bags m ; :: thesis: S1 . b = S2 . b
reconsider b = b as Element of Bags m by A5;
S1 . b = P . ((2 (#) b) +* (0,(b . 0))) by A3
.= S2 . b by A4 ;
hence S1 . b = S2 . b ; :: thesis: verum

end;

hence S1 = S2 ; :: thesis: verum