theorem INVMN2: :: ZMODLAT3:21

for n being Nat
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