theorem Th102: :: MATGRP_0:89

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