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: ( Pre-Lp-Space (M,k) is add-associative & Pre-Lp-Space (M,k) is right_zeroed & Pre-Lp-Space (M,k) is right_complementable & 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 )

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: ( Pre-Lp-Space (M,k) is add-associative & Pre-Lp-Space (M,k) is right_zeroed & Pre-Lp-Space (M,k) is right_complementable & 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 )

proof

thus
Pre-Lp-Space (M,k) is add-associative
:: thesis: ( Pre-Lp-Space (M,k) is right_zeroed & Pre-Lp-Space (M,k) is right_complementable & 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 )
let A1, A2 be Element of (Pre-Lp-Space (M,k)); :: according to RLVECT_1:def 2 :: thesis: A1 + A2 = A2 + A1

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: verum

end;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: verum

proof

thus
Pre-Lp-Space (M,k) is right_zeroed
:: thesis: ( Pre-Lp-Space (M,k) is right_complementable & 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 )
let A1, A2, A3 be Element of (Pre-Lp-Space (M,k)); :: according to RLVECT_1:def 3 :: thesis: (A1 + A2) + A3 = A1 + (A2 + A3)

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: verum

end;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: verum

proof

thus
Pre-Lp-Space (M,k) is right_complementable
:: thesis: ( 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 )
let A1 be Element of (Pre-Lp-Space (M,k)); :: according to RLVECT_1:def 4 :: thesis: A1 + (0. (Pre-Lp-Space (M,k))) = A1

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: verum

end;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: verum

proof

let A1 be Element of (Pre-Lp-Space (M,k)); :: according to ALGSTR_0:def 16 :: thesis: A1 is right_complementable

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: A1 + A2 = 0. (Pre-Lp-Space (M,k))

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: verum

end;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: A1 + A2 = 0. (Pre-Lp-Space (M,k))

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: verum

now :: thesis: for x0, y0 being Real

for A1, A2 being Element of (Pre-Lp-Space (M,k)) holds

( x0 * (A1 + A2) = (x0 * A1) + (x0 * A2) & (x0 + y0) * A1 = (x0 * A1) + (y0 * A1) & (x0 * y0) * A1 = x0 * (y0 * A1) & 1 * A1 = A1 )

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: verumfor A1, A2 being Element of (Pre-Lp-Space (M,k)) holds

( x0 * (A1 + A2) = (x0 * A1) + (x0 * A2) & (x0 + y0) * A1 = (x0 * A1) + (y0 * A1) & (x0 * y0) * A1 = x0 * (y0 * A1) & 1 * A1 = A1 )

let x0, y0 be Real; :: thesis: for A1, A2 being Element of (Pre-Lp-Space (M,k)) holds

( x0 * (A1 + A2) = (x0 * A1) + (x0 * A2) & (x0 + y0) * A1 = (x0 * A1) + (y0 * A1) & (x0 * y0) * A1 = x0 * (y0 * A1) & 1 * A1 = A1 )

let A1, A2 be Element of (Pre-Lp-Space (M,k)); :: thesis: ( x0 * (A1 + A2) = (x0 * A1) + (x0 * A2) & (x0 + y0) * A1 = (x0 * A1) + (y0 * A1) & (x0 * y0) * A1 = x0 * (y0 * A1) & 1 * A1 = A1 )

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: ( (x0 + y0) * A1 = (x0 * A1) + (y0 * A1) & (x0 * y0) * A1 = x0 * (y0 * A1) & 1 * A1 = A1 )

(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 = x0 * (y0 * A1) & 1 * A1 = A1 )

(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 * A1 = A1

1 (#) a = a by A23, RLVECT_1:def 8;

hence 1 * A1 = A1 by A19, A21, Def10, A1; :: thesis: verum

end;( x0 * (A1 + A2) = (x0 * A1) + (x0 * A2) & (x0 + y0) * A1 = (x0 * A1) + (y0 * A1) & (x0 * y0) * A1 = x0 * (y0 * A1) & 1 * A1 = A1 )

let A1, A2 be Element of (Pre-Lp-Space (M,k)); :: thesis: ( x0 * (A1 + A2) = (x0 * A1) + (x0 * A2) & (x0 + y0) * A1 = (x0 * A1) + (y0 * A1) & (x0 * y0) * A1 = x0 * (y0 * A1) & 1 * A1 = A1 )

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: ( (x0 + y0) * A1 = (x0 * A1) + (y0 * A1) & (x0 * y0) * A1 = x0 * (y0 * A1) & 1 * A1 = A1 )

(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 = x0 * (y0 * A1) & 1 * A1 = A1 )

(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 * A1 = A1

1 (#) a = a by A23, RLVECT_1:def 8;

hence 1 * A1 = A1 by A19, A21, Def10, A1; :: thesis: verum