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