let n be set ; :: thesis: for L being non empty add-associative right_zeroed doubleLoopStr
for p, q, r being Series of n,L holds (p + q) + r = p + (q + r)
let L be non empty add-associative right_zeroed doubleLoopStr ; :: thesis: for p, q, r being Series of n,L holds (p + q) + r = p + (q + r)
let p, q, r be Series of n,L; :: thesis: (p + q) + r = p + (q + r)

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

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

end;

hence (p + q) + r = p + (q + r) ; :: thesis: verum