theorem induced_distance_is_distance:
∀R:real.∀V:vector_space R.∀norm:norm ? V.
is_distance ? ? (induced_distance_fun ? ? norm).
theorem induced_distance_is_distance:
∀R:real.∀V:vector_space R.∀norm:norm ? V.
is_distance ? ? (induced_distance_fun ? ? norm).