let R be Ring; :: thesis: for n being Nat
for S being Subring of R
for X being Matrix of n,S holds X is Matrix of n,R
let n be Nat; :: thesis: for S being Subring of R
for X being Matrix of n,S holds X is Matrix of n,R
let S be Subring of R; :: thesis: for X being Matrix of n,S holds X is Matrix of n,R
let X be Matrix of n,S; :: thesis: X is Matrix of n,R
set US = the carrier of S;
set UR = the carrier of R;
( the carrier of S c= the carrier of R & not the carrier of S is empty & not the carrier of R is empty ) by C0SP1:def 3;
hence X is Matrix of n,R by Th81; :: thesis: verum