set M = addLoopStr(# I,(add| (I,R)),(In ((0. R),I)) #);
reconsider M = addLoopStr(# I,(add| (I,R)),(In ((0. R),I)) #) as non empty addLoopStr ;

now :: thesis: for u being object st u in [:I,I:] holds
u in dom the addF of R

let u be object ; :: thesis: ( u in [:I,I:] implies u in dom the addF of R )
A1: dom the addF of R = [: the carrier of R, the carrier of R:] by FUNCT_2:def 1;
assume u in [:I,I:] ; :: thesis: u in dom the addF of R
hence u in dom the addF of R by A1; :: thesis: verum

end;

then [:I,I:] c= dom the addF of R ;
then A2: dom ( the addF of R || I) = [:I,I:] by RELAT_1:62;
A3: for a, b being Element of M
for a9, b9 being Element of I st a9 = a & b9 = b holds
a + b = a9 + b9

proof

let a, b be Element of M; :: thesis: for a9, b9 being Element of I st a9 = a & b9 = b holds
a + b = a9 + b9
let a9, b9 be Element of I; :: thesis: ( a9 = a & b9 = b implies a + b = a9 + b9 )
assume A4: ( a9 = a & b9 = b ) ; :: thesis: a + b = a9 + b9
[a9,b9] in dom ( the addF of R || I) by A2;
hence a + b = a9 + b9 by A4, FUNCT_1:47; :: thesis: verum

end;

now :: thesis: for a, b, c being Element of M holds (a + b) + c = a + (b + c)

let a, b, c be Element of M; :: thesis: (a + b) + c = a + (b + c)
reconsider a9 = a, b9 = b, c9 = c as Element of I ;
a9 + b9 in I by Def1;
then A5: [(a9 + b9),c9] in dom ( the addF of R || I) by A2, ZFMISC_1:def 2;
b9 + c9 in I by Def1;
then A6: [a9,(b9 + c9)] in dom ( the addF of R || I) by A2, ZFMISC_1:def 2;
thus (a + b) + c = ( the addF of R || I) . [(a9 + b9),c9] by A3
.= (a9 + b9) + c9 by A5, FUNCT_1:47
.= a9 + (b9 + c9) by RLVECT_1:def 3
.= (add| (I,R)) . [a9,(b9 + c9)] by A6, FUNCT_1:47
.= a + (b + c) by A3 ; :: thesis: verum

end;

hence Gr (I,R) is add-associative by RLVECT_1:def 3; :: thesis: verum