theorem :: REAL_NS2:34

for n being Nat
for M being Matrix of n,REAL holds
( M is invertible iff MXR2MXF M is invertible )