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

Sq is convergent by Th70;

hence Lp-Space (M,k) is complete by LOPBAN_1:def 15; :: thesis: verum