let R be Ring; :: thesis: for n being Nat
for S being Subring of R holds n -Matrices_over S c= n -Matrices_over R
let n be Nat; :: thesis: for S being Subring of R holds n -Matrices_over S c= n -Matrices_over R
let S be Subring of R; :: thesis: n -Matrices_over S c= n -Matrices_over R
for x being object st x in n -Matrices_over S holds
x in n -Matrices_over R

proof

let x be object ; :: thesis: ( x in n -Matrices_over S implies x in n -Matrices_over R )
assume x in n -Matrices_over S ; :: thesis: x in n -Matrices_over R
then x is Matrix of n,S by MATRIX_1:2;
then x is Matrix of n,R by Th82;
then x is Element of n -Matrices_over R by MATRIX_1:2;
hence x in n -Matrices_over R ; :: thesis: verum

end;

hence n -Matrices_over S c= n -Matrices_over R by TARSKI:def 3; :: thesis: verum