let e1, e2 be Series of O,L; :: thesis: ( ( for b being bag of O holds e1 . b = s . (b * perm) ) & ( for b being bag of O holds e2 . b = s . (b * perm) ) implies e1 = e2 )
assume that
A3: for b being bag of O holds e1 . b = s . (b * perm) and
A4: for b being bag of O holds e2 . b = s . (b * perm) ; :: thesis: e1 = e2

now :: thesis: for b being Element of Bags O holds e1 . b = e2 . b

let b be Element of Bags O; :: thesis: e1 . b = e2 . b
( e1 . b = s . (b * perm) & s . (b * perm) = e2 . b ) by A3, A4;
hence e1 . b = e2 . b ; :: thesis: verum

end;

hence e1 = e2 ; :: thesis: verum