theorem Th80: :: MATGRP_0:68

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