theorem Th38: :: MATGRP_0:28
for R being Ring
for Y being Matrix of 1,R holds Y = (Y * (1,1)) * (1. (R,1))