let n be Nat; :: thesis: S₁[n,fusc . n,fusc . (n + 1)]
n in NAT by ORDINAL1:def 12;
hence S₁[n,fusc . n,fusc . (n + 1)] by Lm4; :: thesis: verum