set C = CosetSet (M,k);
set aC = addCoset (M,k);
set lC = lmultCoset (M,k);
set A = Pre-Lp-Space (M,k);
A1: ( 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 Def11;
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 2 :: thesis:
A1 in CosetSet (M,k) by A1;
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 A1;
then consider b being PartFunc of X,REAL such that
A3: ( A2 = a.e-eq-class_Lp (b,M,k) & b in Lp_Functions (M,k) ) ;
A4: ( a in A1 & b in A2 ) by A2, A3, Th38;
then A1 + A2 = a.e-eq-class_Lp ((a + b),M,k) by A1, Def8;
hence A1 + A2 = A2 + A1 by A1, A4, Def8; :: 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 3 :: thesis:
A1 in CosetSet (M,k) by A1;
then consider a being PartFunc of X,REAL such that
A5: ( A1 = a.e-eq-class_Lp (a,M,k) & a in Lp_Functions (M,k) ) ;
A2 in CosetSet (M,k) by A1;
then consider b being PartFunc of X,REAL such that
A6: ( A2 = a.e-eq-class_Lp (b,M,k) & b in Lp_Functions (M,k) ) ;
A3 in CosetSet (M,k) by A1;
then consider c being PartFunc of X,REAL such that
A7: ( 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 A5, A6, A7, Th38;
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 A1, Def8;
then A9: ( a + b in A1 + A2 & b + c in A2 + A3 ) by A1, Th38, Th25, A5, A6, A7;
reconsider a1 = a, b1 = b, c1 = c as VECTOR of (RLSp_LpFunct (M,k)) by A5, A6, A7;
A10: ( a + b = a1 + b1 & b + c = b1 + c1 ) by Th29;
then a + (b + c) = a1 + (b1 + c1) by Th29;
then a + (b + c) = (a1 + b1) + c1 by RLVECT_1:def 3;
then a + (b + c) = (a + b) + c by A10, Th29;
then (A1 + A2) + A3 = a.e-eq-class_Lp ((a + (b + c)),M,k) by A8, A9, Def8, A1;
hence (A1 + A2) + A3 = A1 + (A2 + A3) by A8, A9, Def8, A1; :: 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 4 :: thesis:
A1 in CosetSet (M,k) by A1;
then consider a being PartFunc of X,REAL such that
A11: ( A1 = a.e-eq-class_Lp (a,M,k) & a in Lp_Functions (M,k) ) ;
A12: a in A1 by A11, Th38;
set z = X --> 0;
A13: X --> 0 in 0. (Pre-Lp-Space (M,k)) by A1, Th38, Th23;
reconsider a1 = a, z1 = X --> 0 as VECTOR of (RLSp_LpFunct (M,k)) by A11, Th23;
a + (X --> 0) = a1 + z1 by Th29
.= a1 + (0. (RLSp_LpFunct (M,k)))
.= a by RLVECT_1:def 4 ;
hence A1 + (0. (Pre-Lp-Space (M,k))) = A1 by A1, A11, A12, A13, Def8; :: 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 A1;
then consider a being PartFunc of X,REAL such that
A14: ( A1 = a.e-eq-class_Lp (a,M,k) & a in Lp_Functions (M,k) ) ;
A15: a in A1 by A14, Th38;
reconsider a1 = a as VECTOR of (RLSp_LpFunct (M,k)) by A14;
A16: (- 1) (#) a in Lp_Functions (M,k) by A14, Th26;
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 A16;
then reconsider A2 = a.e-eq-class_Lp (((- 1) (#) a),M,k) as Element of (Pre-Lp-Space (M,k)) by A1;
take A2 ; :: according to ALGSTR_0:def 11 :: thesis:
A17: (- 1) (#) a in A2 by Th38, A14, Th26;
consider v, g being PartFunc of X,REAL such that
A18: ( 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 Th31;
(- 1) (#) a = (- 1) * a1 by Th30;
then a + ((- 1) (#) a) a.e.= g,M by Th29, A18;
then 0. (Pre-Lp-Space (M,k)) = a.e-eq-class_Lp ((a + ((- 1) (#) a)),M,k) by Th42, A18, A1;
hence A1 + A2 = 0. (Pre-Lp-Space (M,k)) by A15, A17, Def8, A1; :: thesis:

end;

now :: thesis:

let x0, y0 be Real; :: thesis:
let A1, A2 be Element of (Pre-Lp-Space (M,k)); :: thesis:
reconsider x = x0, y = y0 as Real ;
A1 in CosetSet (M,k) by A1;
then consider a being PartFunc of X,REAL such that
A19: ( A1 = a.e-eq-class_Lp (a,M,k) & a in Lp_Functions (M,k) ) ;
A2 in CosetSet (M,k) by A1;
then consider b being PartFunc of X,REAL such that
A20: ( A2 = a.e-eq-class_Lp (b,M,k) & b in Lp_Functions (M,k) ) ;
A21: ( a in A1 & b in A2 ) by A19, A20, Th38;
then (addCoset (M,k)) . (A1,A2) = a.e-eq-class_Lp ((a + b),M,k) by A1, Def8;
then A22: a + b in A1 + A2 by Th38, Th25, A19, A20, A1;
reconsider a1 = a, b1 = b as VECTOR of (RLSp_LpFunct (M,k)) by A19, A20;
A23: ( y (#) a = y * a1 & x (#) a = x * a1 & x (#) b = x * b1 & (x + y) (#) a = (x + y) * a1 & 1 (#) a = 1 * a1 ) by Th30;
a + b = a1 + b1 by Th29;
then x (#) (a + b) = x * (a1 + b1) by Th30;
then x (#) (a + b) = (x * a1) + (x * b1) by RLVECT_1:def 5;
then A24: x (#) (a + b) = (x (#) a) + (x (#) b) by A23, Th29;
(x + y) (#) a = (x * a1) + (y * a1) by A23, RLVECT_1:def 6;
then A25: (x + y) (#) a = (x (#) a) + (y (#) a) by A23, Th29;
x (#) (y (#) a) = x * (y * a1) by A23, Th30
.= (x * y) * a1 by RLVECT_1:def 7 ;
then A26: x (#) (y (#) a) = (x * y) (#) a by Th30;
( (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 A1, A21, Def10;
then A27: ( x (#) a in x * A1 & x (#) b in x * A2 & y (#) a in y * A1 ) by A1, Th38, Th26, A19, A20;
x * (A1 + A2) = a.e-eq-class_Lp (((x (#) a) + (x (#) b)),M,k) by A1, A24, A22, Def10;
hence x0 * (A1 + A2) = (x0 * A1) + (x0 * A2) by A1, A27, Def8; :: thesis:
(x + y) * A1 = a.e-eq-class_Lp (((x (#) a) + (y (#) a)),M,k) by A1, A25, A21, Def10;
hence (x0 + y0) * A1 = (x0 * A1) + (y0 * A1) by A27, Def8, A1; :: thesis:
(x0 * y0) * A1 = a.e-eq-class_Lp ((x (#) (y (#) a)),M,k) by A1, A26, A21, Def10;
hence (x0 * y0) * A1 = x0 * (y0 * A1) by A27, Def10, A1; :: thesis:
1 (#) a = a by A23, RLVECT_1:def 8;
hence 1 * A1 = A1 by A19, A21, Def10, A1; :: 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 ) ; :: thesis: