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

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