let n be Nat; :: thesis: for M being Matrix of n,F_Real st M is Matrix of n,F_Rat & M is invertible holds
M ~ is Matrix of n,F_Rat
let M be Matrix of n,F_Real; :: thesis: ( M is Matrix of n,F_Rat & M is invertible implies M ~ is Matrix of n,F_Rat )
assume that
A1: M is Matrix of n,F_Rat and
A2: M is invertible ; :: thesis: M ~ is Matrix of n,F_Rat
reconsider H = M as Matrix of n,F_Rat by A1;
M ~ = H ~ by A2, INVMN1;
hence M ~ is Matrix of n,F_Rat ; :: thesis: verum