theorem Th2: :: MATRIX_1:2

for x being object
for n being Nat
for K being non empty doubleLoopStr holds
( x is Element of n -Matrices_over K iff x is Matrix of n,K )