let R be non empty add-associative addLoopStr ; :: thesis: for n being Nat
for u, v, w being Tuple of n, the carrier of R holds (u + v) + w = u + (v + w)
let n be Nat; :: thesis: for u, v, w being Tuple of n, the carrier of R holds (u + v) + w = u + (v + w)
let u, v, w be Tuple of n, the carrier of R; :: thesis: (u + v) + w = u + (v + w)
set p = u + v;
set q = v + w;
reconsider u1 = u, v1 = v, w1 = w, p1 = u + v, q2 = v + w as Element of n -tuples_on the carrier of R by FINSEQ_2:131;

now :: thesis: for i being Nat st i in Seg n holds
(p1 + w) . i = (u + q2) . i

let i be Nat; :: thesis: ( i in Seg n implies (p1 + w) . i = (u + q2) . i )
assume AS: i in Seg n ; :: thesis: (p1 + w) . i = (u + q2) . i
reconsider a = u /. i, b = v /. i, c = w /. i as Element of R ;
J: dom v = Seg (len v1) by FINSEQ_1:def 3
.= Seg n by FINSEQ_2:133 ;
K: dom w = Seg (len w1) by FINSEQ_1:def 3
.= Seg n by FINSEQ_2:133 ;
dom u = Seg (len u1) by FINSEQ_1:def 3
.= Seg n by FINSEQ_2:133 ;
then H: ( a = u1 . i & b = v1 . i & c = w1 . i ) by K, J, AS, PARTFUN1:def 6;
then A: p1 . i = a + b by AS, FVSUM_1:18;
B: q2 . i = b + c by AS, H, FVSUM_1:18;
thus (p1 + w) . i = (a + b) + c by AS, A, H, FVSUM_1:18
.= a + (b + c) by RLVECT_1:def 3
.= (u + q2) . i by AS, B, H, FVSUM_1:18 ; :: thesis: verum

end;

hence (u + v) + w = u + (v + w) by FINSEQ_2:119; :: thesis: verum