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