let n be Nat; 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
; verum