realtointM M is Matrix of n,n,INT ;
hence realtointM M is Matrix of n,INT ; :: thesis: verum