theorem Th81: :: MATGRP_0:69

for m, n being Nat
for D, E being non empty set st D c= E holds
for X being Matrix of m,n,D holds X is Matrix of m,n,E