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;

now :: thesis: for a being Element of M holds a + (0. M) = a

let a be Element of M; :: thesis: a + (0. M) = a
reconsider a9 = a as Element of I ;
0. R in I by Th3;
then A3: [a9,(0. R)] in dom ( the addF of R || I) by A2, ZFMISC_1:def 2;
thus a + (0. M) = ( the addF of R || I) . [a9,(0. R)] by Th3, SUBSET_1:def 8
.= a9 + (0. R) by A3, FUNCT_1:47
.= a by RLVECT_1:def 4 ; :: thesis: verum

end;

hence Gr (I,R) is right_zeroed by RLVECT_1:def 4; :: thesis: verum