(4) follows immediately from a version of the open mapping theorem: If a continuous linear operator between between Banach (or Fréchet or even more general) spaces has non-meager range, then it is open and, in particular, surjective.

This is theorem 2.11 in Rudin's *Functional Analysis*. As you said, (5) is an easy consequence. A far more general result is *Grothendieck's factorization theorem*.

The linear continuous images of the *unit balls* of Banach spaces are called *Banach discs*. This is a standard notion in the locally convex theory. It is used, for example, to define ultrabornological locally convex spaces. Without checking, this shoud appear in the *Introduction to Functional Analysis* of Meise and Vogt and it is discussed certainly in *Barrelled Locally Convex Spaces* of Bonet and Perez-Carreras.