theorem Th93: :: MATGRP_0:80

for R being Ring
for n being Nat
for S being Subring of R holds matrix_mult (n,S) = (matrix_mult (n,R)) || (n -Matrices_over S)