let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S holds Pre-L-Space M = Pre-Lp-Space M,1
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S holds Pre-L-Space M = Pre-Lp-Space M,1
let M be sigma_Measure of S; :: thesis: Pre-L-Space M = Pre-Lp-Space M,1
A1: ( the carrier of (Pre-L-Space M) = CosetSet M & the addF of (Pre-L-Space M) = addCoset M & 0. (Pre-L-Space M) = zeroCoset M & the Mult of (Pre-L-Space M) = lmultCoset M ) by LPSPACE1:def 18;
( CosetSet M = CosetSet M,1 & addCoset M = addCoset M,1 & zeroCoset M = zeroCoset M,1 & lmultCoset M = lmultCoset M,1 ) by Th9a, Th9b, Th9c, Th9d;
hence Pre-L-Space M = Pre-Lp-Space M,1 by A1, VSPDef6X; :: thesis: verum