let R be non empty Abelian addLoopStr ; :: thesis: for n being Nat
for u, v being Tuple of n, the carrier of R holds u + v = v + u
let n be Nat; :: thesis: for u, v being Tuple of n, the carrier of R holds u + v = v + u
let u, v be Tuple of n, the carrier of R; :: thesis: u + v = v + u
set w1 = u + v;
set w2 = v + u;
reconsider u1 = u, v1 = v 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
(u + v) . i = (v + u) . i

let i be Nat; :: thesis: ( i in Seg n implies (u + v) . i = (v + u) . i )
assume AS: i in Seg n ; :: thesis: (u + v) . i = (v + u) . i
reconsider a = u /. i, b = v /. i as Element of R ;
J: dom v = Seg (len v1) 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 ) by J, AS, PARTFUN1:def 6;
then (u + v) . i = a + b by AS, FVSUM_1:18
.= (v + u) . i by H, AS, FVSUM_1:18 ;
hence (u + v) . i = (v + u) . i ; :: thesis: verum

end;

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