let p, q be Series of n,L; :: thesis: p + q = q + p

now :: thesis: for b being Element of Bags n holds (p + q) . b = (q + p) . b

let b be Element of Bags n; :: thesis: (p + q) . b = (q + p) . b
thus (p + q) . b = (q . b) + (p . b) by Th15
.= (q + p) . b by Th15 ; :: thesis: verum

end;

hence p + q = q + p ; :: thesis: verum