let m, n be non zero Element of NAT ; :: thesis: for M being Matrix of m,F_Real holds
( Mx2Tran M is bijective iff M is invertible )
let M be Matrix of m,F_Real; :: thesis: ( Mx2Tran M is bijective iff M is invertible )
( M is invertible iff Det M <> 0. F_Real ) by LAPLACE:34;
hence ( Mx2Tran M is bijective iff M is invertible ) by MATRTOP1:40, MATRTOP1:42; :: thesis: verum