take Complex_l2_Space ; :: thesis: Complex_l2_Space is complete
thus Complex_l2_Space is complete ; :: thesis: verum