theorem Th89: :: MATGRP_0:76

for R being Ring
for n being Nat
for S being Subring of R
for b being Matrix of n,S
for B being Matrix of n,R st b = B holds
for j being Nat st j in Seg (width b) holds
Col (b,j) = Col (B,j)