for n being Nat
for A, B being Matrix of n,F_Real st Det A <> 0. F_Real holds
( (Mx2Tran A) " = Mx2Tran B iff A ~ = B )