In this article, we formalized L1 space formed by complexvalued partial functions [11], [15]. The real-valued case was formalized in [22] and this article is its generalization.
