theorem :: CLASSES4:71

for UN being non trivial Universe
for D being non empty set st D in UN holds
for M being Matrix of D holds M in UN by Th64, Th69;