let n be Nat; :: thesis: uInt . n = No_uOrdinal_op n
( uInt . n = No_Ordinal_op n & No_Ordinal_op n == No_uOrdinal_op n ) by Th72, Th73;
hence uInt . n = No_uOrdinal_op n by SURREALO:50; :: thesis: verum