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

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

end;

then [:I,I:] c= dom the addF of R by TARSKI:def 3;
then A2: dom (the addF of R || I) = [:I,I:] by RELAT_1:91;
A3: for a, b being Element of M
for a', b' being Element of I st a' = a & b' = b holds
a + b = a' + b'

proof

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

end;

now

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

end;

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