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