theorem :: NDIFF11:9

for m, n being non zero Element of NAT
for M being Matrix of m,F_Real holds
( Mx2Tran M is bijective iff Det M <> 0. F_Real ) by MATRTOP1:40, MATRTOP1:42;