for Sq being sequence of (Lp-Space (M,k)) st Sq is CCauchy holds
Sq is convergent by Th006;
hence Lp-Space (M,k) is complete by LOPBAN_1:def 16; :: thesis: verum