Let x0 of type ι be given.

Assume H0: SNo x0.

Assume H1: SNoLt 0 x0.

Let x1 of type ι → ι be given.

Assume H2: ∀ x2 . x2 ∈ SNoS_ (SNoLev x0) ⟶ SNoLt 0 x2 ⟶ and (SNo (x1 x2)) (mul_SNo x2 (x1 x2) = 1).

Apply and3I with ∀ x2 . x2 ∈ famunion omega (λ x3 . ap (SNo_recipaux x0 x1 x3) 0) ⟶ SNo x2, ∀ x2 . x2 ∈ famunion omega (λ x3 . ap (SNo_recipaux x0 x1 x3) 1) ⟶ SNo x2, ∀ x2 . x2 ∈ famunion omega (λ x3 . ap (SNo_recipaux x0 x1 x3) 0) ⟶ ∀ x3 . x3 ∈ famunion omega (λ x4 . ap (SNo_recipaux x0 x1 x4) 1) ⟶ SNoLt x2 x3 leaving 3 subgoals.

Let x2 of type ι be given.

Assume H3: x2 ∈ famunion omega (λ x3 . ap (SNo_recipaux x0 x1 x3) 0).

Apply famunionE_impred with omega, λ x3 . ap (SNo_recipaux x0 x1 x3) 0, x2, SNo x2 leaving 2 subgoals.

The subproof is completed by applying H3.

Let x3 of type ι be given.

Assume H4: x3 ∈ omega.

Assume H5: x2 ∈ ap (SNo_recipaux x0 x1 x3) 0.

Apply SNo_recipaux_lem1 with x0, x1, x3, SNo x2 leaving 5 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

The subproof is completed by applying H2.

Apply omega_nat_p with x3.

The subproof is completed by applying H4.

Assume H6: ∀ x4 . x4 ∈ ap (SNo_recipaux x0 x1 x3) 0 ⟶ and (SNo x4) (SNoLt (mul_SNo x0 x4) 1).

Assume H7: ∀ x4 . x4 ∈ ap (SNo_recipaux x0 x1 x3) 1 ⟶ and (SNo x4) (SNoLt 1 (mul_SNo x0 x4)).

Apply H6 with x2, SNo x2 leaving 2 subgoals.

The subproof is completed by applying H5.

Assume H8: SNo x2.

Assume H9: SNoLt (mul_SNo x0 x2) 1.

The subproof is completed by applying H8.