inttorealM M is Matrix of n,n,REAL ;
hence inttorealM M is Matrix of n,REAL ; :: thesis: verum