set C = CosetSet (M,k);
set aC = addCoset (M,k);
set lC = 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;
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: