case H
V : Type ?u.476976
V₁ : Type u_3
V₂ : Type u_1
V₃ : Type u_2
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g : NormedAddGroupHom V₁ V₂
f : NormedAddGroupHom V₂ V₃
x✝ : V₁
⊢ ↑(NormedAddGroupHom.comp f 0) x✝ = ↑0 x✝
V : Type ?u.476976
V₁ : Type u_3
V₂ : Type u_1
V₃ : Type u_2
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g : NormedAddGroupHom V₁ V₂
f : NormedAddGroupHom V₂ V₃
⊢ NormedAddGroupHom.comp f 0 = 0
ext
no goals
case H
V : Type ?u.476976
V₁ : Type u_3
V₂ : Type u_1
V₃ : Type u_2
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g : NormedAddGroupHom V₁ V₂
f : NormedAddGroupHom V₂ V₃
x✝ : V₁
⊢ ↑(NormedAddGroupHom.comp f 0) x✝ = ↑0 x✝
exact map_zero f