theorem Th5: :: TOPREALB:5

R^1 | (R^1 ([#] REAL)) = R^1