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 )
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 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 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:70; :: thesis: verum

end;

reconsider I = I as RightIdeal of R ;
M is right_complementable

proof

let a be Element of M; :: according to ALGSTR_0:def 16 :: thesis: a is right_complementable
reconsider a9 = a as Element of I ;
reconsider b = - a9 as Element of M by Th14;
a + b = a9 + (- a9) by A3
.= 0. R by RLVECT_1:16
.= 0. M by Th3, FUNCT_7:def 1 ;
hence ex b being Element of M st a + b = 0. M ; :: according to ALGSTR_0:def 11 :: thesis: verum

end;

hence Gr I,R is right_complementable ; :: thesis: verum