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 Th71, Th72, Th73, Th74;
hence Pre-L-Space M = Pre-Lp-Space (M,1) by A1, Def11; :: thesis: verum