Let x0 of type ι be given.

Assume H0: x0 ∈ int.

Let x1 of type ο be given.

Assume H1: ∀ x2 . and (x2 ∈ omega) (∃ x3 . and (x3 ∈ int) (x0 = mul_SNo (eps_ x2) x3)) ⟶ x1.

Apply H1 with 0.

Apply andI with 0 ∈ omega, ∃ x2 . and (x2 ∈ int) (x0 = mul_SNo (eps_ 0) x2) leaving 2 subgoals.

Apply nat_p_omega with 0.

The subproof is completed by applying nat_0.

Let x2 of type ο be given.

Assume H2: ∀ x3 . and (x3 ∈ int) (x0 = mul_SNo (eps_ 0) x3) ⟶ x2.

Apply H2 with x0.

Apply andI with x0 ∈ int, x0 = mul_SNo (eps_ 0) x0 leaving 2 subgoals.

The subproof is completed by applying H0.

Apply eps_0_1 with λ x3 x4 . x0 = mul_SNo x4 x0.

Let x3 of type ι → ι → ο be given.

Apply mul_SNo_oneL with x0, λ x4 x5 . x3 x5 x4.

Apply int_SNo with x0.

The subproof is completed by applying H0.

■

Proofgold Proof