theorem :: MATGRP_0:65

for n being Nat
for L being non empty doubleLoopStr holds 1. (L,n) is Element of (Matrix_ring (n,L)) ;