let r1, r2 be Series of n,L; :: thesis: ( ( for b being bag of n holds r1 . b = p . (b bag_extend 0) ) & ( for b being bag of n holds r2 . b = p . (b bag_extend 0) ) implies r1 = r2 )
assume that
A3: for b being bag of n holds r1 . b = p . (b bag_extend 0) and
A4: for b being bag of n holds r2 . b = p . (b bag_extend 0) ; :: thesis: r1 = r2

now :: thesis: for b being Element of Bags n holds r1 . b = r2 . b

let b be Element of Bags n; :: thesis: r1 . b = r2 . b
r1 . b = p . (b bag_extend 0) by A3;
hence r1 . b = r2 . b by A4; :: thesis: verum

end;

hence r1 = r2 ; :: thesis: verum