Assume H1: atleastp real ω.
Apply equip_sym real (𝒫 ω) equip_real_Power_omega to the current goal.
Let f be given.
Assume Hf: bij (𝒫 ω) real f.
Apply H1 to the current goal.
Let g be given.
Assume Hg: inj real ω g.
Apply form100_22_v2 (λx ⇒ g (f x)) to the current goal.
We will prove inj (𝒫 ω) ω (λx ⇒ g (f x)).
An exact proof term for the current goal is inj_comp (𝒫 ω) real ω f g (bij_inj (𝒫 ω) real f Hf) Hg.
∎