no goals
F : Type ?u.1016366
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
C : ℝ
⊢ ‖normComp f‖ = ‖f‖
simp only [norm_eq, coe_normComp, norm_norm, Function.comp]