theorem PiBase.WellDefined.functionallyT2Space : WellDefined FunctionallyT2Space

theorem PiBase.Homeomorph.functionallyT2Space {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] [h : FunctionallyT2Space X] (f : X ≃ₜ Y) : FunctionallyT2Space Y