take Complex_l1_Space ; :: thesis: Complex_l1_Space is complete
thus Complex_l1_Space is complete by Def14, CSSPACE3:9; :: thesis: verum