theorem Th20: :: MATRIX_7:21

for G being Group holds (<*> the carrier of G) " = <*> the carrier of G