Let x0 of type ι be given.

Assume H0: x0 ∈ omega.

Let x1 of type ο be given.

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

Apply H1 with x0.

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

The subproof is completed by applying H0.

Let x2 of type ο be given.

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

Apply H2 with 1.

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

Apply Subq_omega_int with 1.

Apply nat_p_omega with 1.

The subproof is completed by applying nat_1.

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

Apply mul_SNo_oneR with eps_ x0, λ x4 x5 . x3 x5 x4.

Apply SNo_eps_ with x0.

The subproof is completed by applying H0.

■

Proofgold Proof