theorem Th101: :: MATGRP_0:88

for R being Ring
for n being Nat
for x, y being Element of R holds (x * (1. (R,n))) * y = (x * y) * (1. (R,n))