theorem Th88: :: MATGRP_0:75

for R being Ring
for n being Nat
for S being Subring of R
for a being Matrix of n,S
for A being Matrix of n,R st a = A holds
for i being Nat st i in dom a holds
Line (a,i) = Line (A,i)