theorem REALTOINT: :: ZMATRLIN:5

for D, E being non empty set
for M being Matrix of D st ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) in E ) holds
M is Matrix of E