for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for k being geq_than_1 Real
for Sq being sequence of (Lp-Space (M,k)) st Sq is Cauchy_sequence_by_Norm holds
Sq is convergent