let n be Nat; :: thesis: uInt . n = No_Ordinal_op n
defpred S₁[ Nat] means uInt . $1 = No_Ordinal_op $1;
A1: S₁[ 0 ] by Def1, Th64;
A2: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A3: S₁[m] ; :: thesis: S₁[m + 1]
Segm (m + 1) = succ (Segm m) by NAT_1:38;
hence No_Ordinal_op (m + 1) = [{(No_Ordinal_op m)},{}] by Th65
.= uInt . (m + 1) by Def1, A3 ;
:: thesis: verum

end;

for m being Nat holds S₁[m] from NAT_1:sch 2(A1, A2);
hence uInt . n = No_Ordinal_op n ; :: thesis: verum