let L be non empty add-associative addLoopStr ; :: thesis: for p, q, r being sequence of L holds (p + q) + r = p + (q + r)
let p, q, r be sequence of L; :: thesis: (p + q) + r = p + (q + r)
now :: thesis: for n being Element of NAT holds ((p + q) + r) . n = (p + (q + r)) . n
let n be Element of NAT ; :: thesis: ((p + q) + r) . n = (p + (q + r)) . n
thus ((p + q) + r) . n = ((p + q) . n) + (r . n) by NORMSP_1:def 2
.= ((p . n) + (q . n)) + (r . n) by NORMSP_1:def 2
.= (p . n) + ((q . n) + (r . n)) by RLVECT_1:def 3
.= (p . n) + ((q + r) . n) by NORMSP_1:def 2
.= (p + (q + r)) . n by NORMSP_1:def 2 ; :: thesis: verum
end;
hence (p + q) + r = p + (q + r) ; :: thesis: verum