theorem Th82: :: MATGRP_0:70
for R being Ring
for n being Nat
for S being Subring of R
for X being Matrix of n,S holds X is Matrix of n,R