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

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 5
.= ((p . n) + (q . n)) + (r . n) by NORMSP_1:def 5
.= (p . n) + ((q . n) + (r . n)) by RLVECT_1:def 6
.= (p . n) + ((q + r) . n) by NORMSP_1:def 5
.= (p + (q + r)) . n by NORMSP_1:def 5 ; :: thesis: verum

end;

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