Let Y, Z and x be given.
Assume HY HZ Hx.
We will prove (⋃y ∈ Y{(x + y * z) :/: (y + z)|z ∈ Z, 0 < y + z}) ⊆ real.
Let w be given.
Assume Hw.
Apply famunionE_impred Y (λy ⇒ {(x + y * z) :/: (y + z)|z ∈ Z, 0 < y + z}) w Hw to the current goal.
Let y be given.
Assume Hy: y ∈ Y.
Assume Hw2: w ∈ {(x + y * z) :/: (y + z)|z ∈ Z, 0 < y + z}.
Apply ReplSepE_impred Z (λz ⇒ 0 < y + z) (λz ⇒ (x + y * z) :/: (y + z)) w Hw2 to the current goal.
Let z be given.
Assume Hz: z ∈ Z.
Assume Hyz: 0 < y + z.
Assume Hw3: w = (x + y * z) :/: (y + z).
We will prove w ∈ real.
rewrite the current goal using Hw3 (from left to right).
Apply real_div_SNo to the current goal.
We will prove x + y * z ∈ real.
Apply real_add_SNo to the current goal.
An exact proof term for the current goal is Hx.
Apply real_mul_SNo to the current goal.
An exact proof term for the current goal is HY y Hy.
An exact proof term for the current goal is HZ z Hz.
We will prove y + z ∈ real.
Apply real_add_SNo to the current goal.
An exact proof term for the current goal is HY y Hy.
An exact proof term for the current goal is HZ z Hz.
∎