theorem Th72: :: MATGRP_0:60

for n being Nat
for L being non empty doubleLoopStr
for x being object holds
( x is Element of (Matrix_ring (n,L)) iff x is Matrix of n,L ) by MATRIX_1:2;