for G being addGroup holds Right_Cosets ((0). G) = { {a} where a is Element of G : verum }