theorem :: ANPROJ_8:18

for n being Nat
for M being Matrix of n,REAL
for N being Matrix of n,F_Real st M = N holds
( M is invertible iff N is invertible )