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 ;
then
[:I,I:] c= dom the addF of R
;
then A2:
dom ( the addF of R || I) = [:I,I:]
by RELAT_1:62;
hence
Gr (I,R) is right_zeroed
by RLVECT_1:def 4; verum