(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.

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.

(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.