theorem Th33: :: MATRTOP1:33

for n being Nat holds Mx2Tran (1. (F_Real,n)) = id (TOP-REAL n)