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