theorem Th87: :: MATGRP_0:74

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