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