theorem :: MATGRP_0:27

for R being Ring
for r, s being Element of R holds
( r * <*<*s*>*> = <*<*(r * s)*>*> & <*<*s*>*> * r = <*<*(s * r)*>*> )