theorem :: SURREALN:78

for n being Nat holds uInt . n = No_uOrdinal_op n