theorem INVMN1: :: ZMODLAT3:20

for n being Nat
for M being Matrix of n,F_Real
for H being Matrix of n,F_Rat st M = H & M is invertible holds
( H is invertible & M ~ = H ~ )