set C = CosetSet M,k;
set aC = addCoset M,k;
set zC = zeroCoset M,k;
set lC = lmultCoset M,k;
set AA = RLSStruct(# (CosetSet M,k),(zeroCoset M,k),(addCoset M,k),(lmultCoset M,k) #);
set A = Pre-Lp-Space M,k;
A0: ( the carrier of (Pre-Lp-Space M,k) = CosetSet M,k & the addF of (Pre-Lp-Space M,k) = addCoset M,k & 0. (Pre-Lp-Space M,k) = zeroCoset M,k & the Mult of (Pre-Lp-Space M,k) = lmultCoset M,k ) by VSPDef6X;
thus Pre-Lp-Space M,k is Abelian :: thesis:

proof

let A1, A2 be Element of (Pre-Lp-Space M,k); :: according to RLVECT_1:def 5 :: thesis:
A1 in CosetSet M,k by A0;
then consider a being PartFunc of X,REAL such that
A2: ( A1 = a.e-eq-class_Lp a,M,k & a in Lp_Functions M,k ) ;
A2 in CosetSet M,k by A0;
then consider b being PartFunc of X,REAL such that
A4: ( A2 = a.e-eq-class_Lp b,M,k & b in Lp_Functions M,k ) ;
A3: ( a in A1 & b in A2 ) by A2, A4, EQC01;
then A1 + A2 = a.e-eq-class_Lp (a + b),M,k by A0, VSPDef3X;
hence A1 + A2 = A2 + A1 by A0, A3, VSPDef3X; :: thesis:

end;

thus Pre-Lp-Space M,k is add-associative :: thesis:

proof

let A1, A2, A3 be Element of (Pre-Lp-Space M,k); :: according to RLVECT_1:def 6 :: thesis:
A1 in CosetSet M,k by A0;
then consider a being PartFunc of X,REAL such that
A7: ( A1 = a.e-eq-class_Lp a,M,k & a in Lp_Functions M,k ) ;
A2 in CosetSet M,k by A0;
then consider b being PartFunc of X,REAL such that
A9: ( A2 = a.e-eq-class_Lp b,M,k & b in Lp_Functions M,k ) ;
A3 in CosetSet M,k by A0;
then consider c being PartFunc of X,REAL such that
A11: ( A3 = a.e-eq-class_Lp c,M,k & c in Lp_Functions M,k ) ;
A8: ( a in A1 & b in A2 & c in A3 ) by A7, A9, A11, EQC01;
then ( (addCoset M,k) . A1,A2 = a.e-eq-class_Lp (a + b),M,k & (addCoset M,k) . A2,A3 = a.e-eq-class_Lp (b + c),M,k ) by A0, VSPDef3X;
then A15: ( a + b in A1 + A2 & b + c in A2 + A3 ) by A0, EQC01, Th01aLp, A7, A9, A11;
reconsider a1 = a, b1 = b, c1 = c as VECTOR of (RLSp_LpFunct M,k) by A7, A9, A11;
A17: ( a + b = a1 + b1 & b + c = b1 + c1 ) by ThB10;
then a + (b + c) = a1 + (b1 + c1) by ThB10;
then a + (b + c) = (a1 + b1) + c1 by RLVECT_1:def 6;
then a + (b + c) = (a + b) + c by A17, ThB10;
then (A1 + A2) + A3 = a.e-eq-class_Lp (a + (b + c)),M,k by A8, A15, VSPDef3X, A0;
hence (A1 + A2) + A3 = A1 + (A2 + A3) by A8, A15, VSPDef3X, A0; :: thesis:

end;

thus Pre-Lp-Space M,k is right_zeroed :: thesis:

proof

let A1 be Element of (Pre-Lp-Space M,k); :: according to RLVECT_1:def 7 :: thesis:
A1 in CosetSet M,k by A0;
then consider a being PartFunc of X,REAL such that
A20: ( A1 = a.e-eq-class_Lp a,M,k & a in Lp_Functions M,k ) ;
A21: a in A1 by A20, EQC01;
reconsider a1 = a as VECTOR of (RLSp_LpFunct M,k) by A20;
set z = X --> 0 ;
A23: X --> 0 in 0. (Pre-Lp-Space M,k) by A0, EQC01, LmDef1Lp;
reconsider a1 = a, z1 = X --> 0 as VECTOR of (RLSp_LpFunct M,k) by A20, LmDef1Lp;
a + (X --> 0 ) = a1 + z1 by ThB10
.= a1 + (0. (RLSp_LpFunct M,k)) by Th09a
.= a by RLVECT_1:def 7 ;
hence A1 + (0. (Pre-Lp-Space M,k)) = A1 by A0, A20, A21, A23, VSPDef3X; :: thesis:

end;

thus Pre-Lp-Space M,k is right_complementable :: thesis:

proof

let A1 be Element of (Pre-Lp-Space M,k); :: according to ALGSTR_0:def 16 :: thesis:
A1 in CosetSet M,k by A0;
then consider a being PartFunc of X,REAL such that
A26: ( A1 = a.e-eq-class_Lp a,M,k & a in Lp_Functions M,k ) ;
A27: a in A1 by A26, EQC01;
reconsider a1 = a as VECTOR of (RLSp_LpFunct M,k) by A26;
A28: (- 1) (#) a in Lp_Functions M,k by A26, Th01bLp;
set A2 = a.e-eq-class_Lp ((- 1) (#) a),M,k;
a.e-eq-class_Lp ((- 1) (#) a),M,k in CosetSet M,k by A28;
then reconsider A2 = a.e-eq-class_Lp ((- 1) (#) a),M,k as Element of (Pre-Lp-Space M,k) by A0;
take A2 ; :: according to ALGSTR_0:def 11 :: thesis:
A29: (- 1) (#) a in A2 by EQC01, A26, Th01bLp;
consider v, g being PartFunc of X,REAL such that
A30: ( v in Lp_Functions M,k & g in Lp_Functions M,k & v = a1 + ((- 1) * a1) & g = X --> 0 & v a.e.= g,M ) by ThB11Z;
(- 1) (#) a = (- 1) * a1 by ThB11;
then a + ((- 1) (#) a) a.e.= g,M by ThB10, A30;
then 0. (Pre-Lp-Space M,k) = a.e-eq-class_Lp (a + ((- 1) (#) a)),M,k by EQC02bx, A30, A0;
hence A1 + A2 = 0. (Pre-Lp-Space M,k) by A27, A29, VSPDef3X, A0; :: thesis:

end;

now

let x0, y0 be real number ; :: thesis:
let A1, A2 be Element of (Pre-Lp-Space M,k); :: thesis:
reconsider x = x0, y = y0 as Real by XREAL_0:def 1;
A1 in CosetSet M,k by A0;
then consider a being PartFunc of X,REAL such that
A35: ( A1 = a.e-eq-class_Lp a,M,k & a in Lp_Functions M,k ) ;
A2 in CosetSet M,k by A0;
then consider b being PartFunc of X,REAL such that
A37: ( A2 = a.e-eq-class_Lp b,M,k & b in Lp_Functions M,k ) ;
A36: ( a in A1 & b in A2 ) by A35, A37, EQC01;
then (addCoset M,k) . A1,A2 = a.e-eq-class_Lp (a + b),M,k by A0, VSPDef3X;
then A40: a + b in A1 + A2 by EQC01, Th01aLp, A35, A37, A0;
reconsider a1 = a, b1 = b as VECTOR of (RLSp_LpFunct M,k) by A35, A37;
A42: ( y (#) a = y * a1 & x (#) a = x * a1 & x (#) b = x * b1 & (x + y) (#) a = (x + y) * a1 & 1 (#) a = 1 * a1 ) by ThB11;
a + b = a1 + b1 by ThB10;
then x (#) (a + b) = x * (a1 + b1) by ThB11;
then x (#) (a + b) = (x * a1) + (x * b1) by RLVECT_1:def 8;
then A45: x (#) (a + b) = (x (#) a) + (x (#) b) by A42, ThB10;
(x + y) (#) a = (x * a1) + (y * a1) by A42, RLVECT_1:def 9;
then A46: (x + y) (#) a = (x (#) a) + (y (#) a) by A42, ThB10;
x (#) (y (#) a) = x * (y * a1) by A42, ThB11
.= (x * y) * a1 by RLVECT_1:def 10 ;
then A48: x (#) (y (#) a) = (x * y) (#) a by ThB11;
( (lmultCoset M,k) . x,A1 = a.e-eq-class_Lp (x (#) a),M,k & (lmultCoset M,k) . x,A2 = a.e-eq-class_Lp (x (#) b),M,k & (lmultCoset M,k) . y,A1 = a.e-eq-class_Lp (y (#) a),M,k ) by A0, A36, VSPDef5X;
then A49: ( x (#) a in x * A1 & x (#) b in x * A2 & y (#) a in y * A1 ) by A0, EQC01, Th01bLp, A35, A37;
x * (A1 + A2) = a.e-eq-class_Lp ((x (#) a) + (x (#) b)),M,k by A0, A45, A40, VSPDef5X;
hence x0 * (A1 + A2) = (x0 * A1) + (x0 * A2) by A0, A49, VSPDef3X; :: thesis:
(x + y) * A1 = a.e-eq-class_Lp ((x (#) a) + (y (#) a)),M,k by A0, A46, A36, VSPDef5X;
hence (x0 + y0) * A1 = (x0 * A1) + (y0 * A1) by A49, VSPDef3X, A0; :: thesis:
(x0 * y0) * A1 = a.e-eq-class_Lp (x (#) (y (#) a)),M,k by A0, A48, A36, VSPDef5X;
hence (x0 * y0) * A1 = x0 * (y0 * A1) by A49, VSPDef5X, A0; :: thesis:
1 (#) a = a by A42, RLVECT_1:def 11;
hence 1 * A1 = A1 by A35, A36, VSPDef5X, A0; :: thesis:

end;

hence ( Pre-Lp-Space M,k is vector-distributive & Pre-Lp-Space M,k is scalar-distributive & Pre-Lp-Space M,k is scalar-associative & Pre-Lp-Space M,k is scalar-unital ) by RLVECT_1:def 8, RLVECT_1:def 9, RLVECT_1:def 10, RLVECT_1:def 11; :: thesis: