theorem Th139: :: MATGRP_0:121

for R being Ring
for n being Nat
for S being Subring of R
for M1 being Matrix of n,R
for M2 being Matrix of n,S st M1 = M2 & M2 is invertible holds
M1 is invertible