let n be Nat; :: thesis: for A being Matrix of n,F_Real holds
( Mx2Tran A is one-to-one iff Det A <> 0. F_Real )
let A be Matrix of n,F_Real; :: thesis: ( Mx2Tran A is one-to-one iff Det A <> 0. F_Real )
( Mx2Tran A is one-to-one iff the_rank_of A = n ) by Th39;
hence ( Mx2Tran A is one-to-one iff Det A <> 0. F_Real ) by MATRIX13:83; :: thesis: verum