let n be Nat; ( n > 0 implies (uInt . n) " == uReal . (1 / n) )
assume A1:
n > 0
; (uInt . n) " == uReal . (1 / n)
then
( 0_No = uInt . 0 & uInt . 0 < uInt . n )
by Th9, Def1;
then A2:
not uInt . n == 0_No
;
A3:
n * (1 / n) = 1
by A1, XCMPLX_1:106;
( uInt . n = uDyadic . n & uDyadic . n = uReal . n )
by Def5, Th46;
then
( (uInt . n) * (uReal . (1 / n)) == uReal . 1 & uReal . 1 = 1_No )
by A3, Th57, Th48;
hence
(uInt . n) " == uReal . (1 / n)
by SURREALI:42, A2; verum