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

now

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

end;

hence p + q = q + p by FUNCT_2:63; :: thesis: verum