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;

now

let a be Element of M; :: thesis: a + (0. M) = a
reconsider a' = a as Element of I ;
0. R in I by Th3;
then A3: [a',(0. R)] in dom (the addF of R || I) by A2, ZFMISC_1:def 2;
thus a + (0. M) = (the addF of R || I) . [a',(0. R)] by Th3, FUNCT_7:def 1
.= a' + (0. R) by A3, FUNCT_1:70
.= a by RLVECT_1:def 7 ; :: thesis: verum

end;

hence Gr I,R is right_zeroed by RLVECT_1:def 7; :: thesis: verum