set T = Mx2Tran A;
A1: ( Mx2Tran A is continuous & Mx2Tran (A ~) is continuous ) by Th47;
A2: Det A <> 0. F_Real by LAPLACE:34;
then A3: (Mx2Tran A) " = Mx2Tran (A ~) by Th43;
A4: ( Mx2Tran A is onto & Mx2Tran A is one-to-one ) by A2, Th40, Th42;
then A5: rng (Mx2Tran A) = [#] (TOP-REAL n) by FUNCT_2:def 3;
( dom (Mx2Tran A) = [#] (TOP-REAL n) & (Mx2Tran A) /" = (Mx2Tran A) " ) by A4, FUNCT_2:def 1, TOPS_2:def 4;
hence Mx2Tran A is being_homeomorphism by A4, A3, A1, A5, TOPS_2:def 5; :: thesis: verum