let n be Nat; :: thesis: Mx2Tran (1. (F_Real,n)) = id (TOP-REAL n)
set V = n -VectSp_over F_Real;
reconsider Bn = MX2FinS (1. (F_Real,n)) as OrdBasis of n -VectSp_over F_Real by MATRLIN2:45;
A1: len Bn = n by Th19;
then reconsider ONE = 1. (F_Real,n) as Matrix of len Bn, len Bn,F_Real ;
A2: Mx2Tran (1. (F_Real,n)) = Mx2Tran (ONE,Bn,Bn) by Th20;
A3: [#] (TOP-REAL n) = dom (Mx2Tran (1. (F_Real,n))) by FUNCT_2:def 1
.= [#] (n -VectSp_over F_Real) by A2, FUNCT_2:def 1 ;
thus Mx2Tran (1. (F_Real,n)) = Mx2Tran ((AutMt ((id (n -VectSp_over F_Real)),Bn,Bn)),Bn,Bn) by A1, Th20, MATRLIN2:28
.= id (TOP-REAL n) by A3, MATRLIN2:34 ; :: thesis: verum