theorem Th40: :: MATRTOP1:40

for n being Nat
for A being Matrix of n,F_Real holds
( Mx2Tran A is one-to-one iff Det A <> 0. F_Real )