set C = CosetSet (M,k);

defpred S_{1}[ set , set , set ] means for a, b being PartFunc of X,REAL st a in $1 & b in $2 holds

$3 = a.e-eq-class_Lp ((a + b),M,k);

A6: for A, B being Element of CosetSet (M,k) holds S_{1}[A,B,f . (A,B)]
from BINOP_1:sch 3(A1);

reconsider f = f as BinOp of (CosetSet (M,k)) ;

take f ; :: thesis: for A, B being Element of CosetSet (M,k)

for a, b being PartFunc of X,REAL st a in A & b in B holds

f . (A,B) = a.e-eq-class_Lp ((a + b),M,k)

let A, B be Element of CosetSet (M,k); :: thesis: for a, b being PartFunc of X,REAL st a in A & b in B holds

f . (A,B) = a.e-eq-class_Lp ((a + b),M,k)

let a, b be PartFunc of X,REAL; :: thesis: ( a in A & b in B implies f . (A,B) = a.e-eq-class_Lp ((a + b),M,k) )

assume ( a in A & b in B ) ; :: thesis: f . (A,B) = a.e-eq-class_Lp ((a + b),M,k)

hence f . (A,B) = a.e-eq-class_Lp ((a + b),M,k) by A6; :: thesis: verum

defpred S

$3 = a.e-eq-class_Lp ((a + b),M,k);

A1: now :: thesis: for A, B being Element of CosetSet (M,k) ex z being Element of CosetSet (M,k) st S_{1}[A,B,z]

consider f being Function of [:(CosetSet (M,k)),(CosetSet (M,k)):],(CosetSet (M,k)) such that let A, B be Element of CosetSet (M,k); :: thesis: ex z being Element of CosetSet (M,k) st S_{1}[A,B,z]

A in CosetSet (M,k) ;

then consider a being PartFunc of X,REAL such that

A2: ( A = a.e-eq-class_Lp (a,M,k) & a in Lp_Functions (M,k) ) ;

A3: ex E being Element of S st

( M . (E `) = 0 & dom a = E & a is E -measurable ) by A2, Th35;

B in CosetSet (M,k) ;

then consider b being PartFunc of X,REAL such that

A4: ( B = a.e-eq-class_Lp (b,M,k) & b in Lp_Functions (M,k) ) ;

A5: ex E being Element of S st

( M . (E `) = 0 & dom b = E & b is E -measurable ) by A4, Th35;

set z = a.e-eq-class_Lp ((a + b),M,k);

a + b in Lp_Functions (M,k) by Th25, A2, A4;

then a.e-eq-class_Lp ((a + b),M,k) in CosetSet (M,k) ;

then reconsider z = a.e-eq-class_Lp ((a + b),M,k) as Element of CosetSet (M,k) ;

take z = z; :: thesis: S_{1}[A,B,z]

_{1}[A,B,z]
; :: thesis: verum

end;A in CosetSet (M,k) ;

then consider a being PartFunc of X,REAL such that

A2: ( A = a.e-eq-class_Lp (a,M,k) & a in Lp_Functions (M,k) ) ;

A3: ex E being Element of S st

( M . (E `) = 0 & dom a = E & a is E -measurable ) by A2, Th35;

B in CosetSet (M,k) ;

then consider b being PartFunc of X,REAL such that

A4: ( B = a.e-eq-class_Lp (b,M,k) & b in Lp_Functions (M,k) ) ;

A5: ex E being Element of S st

( M . (E `) = 0 & dom b = E & b is E -measurable ) by A4, Th35;

set z = a.e-eq-class_Lp ((a + b),M,k);

a + b in Lp_Functions (M,k) by Th25, A2, A4;

then a.e-eq-class_Lp ((a + b),M,k) in CosetSet (M,k) ;

then reconsider z = a.e-eq-class_Lp ((a + b),M,k) as Element of CosetSet (M,k) ;

take z = z; :: thesis: S

now :: thesis: for a1, b1 being PartFunc of X,REAL st a1 in A & b1 in B holds

z = a.e-eq-class_Lp ((a1 + b1),M,k)

hence
Sz = a.e-eq-class_Lp ((a1 + b1),M,k)

let a1, b1 be PartFunc of X,REAL; :: thesis: ( a1 in A & b1 in B implies z = a.e-eq-class_Lp ((a1 + b1),M,k) )

assume ( a1 in A & b1 in B ) ; :: thesis: z = a.e-eq-class_Lp ((a1 + b1),M,k)

then ( a1 a.e.= a,M & b1 a.e.= b,M ) by A2, A3, A4, A5, Th37;

hence z = a.e-eq-class_Lp ((a1 + b1),M,k) by Th42, LPSPACE1:31; :: thesis: verum

end;assume ( a1 in A & b1 in B ) ; :: thesis: z = a.e-eq-class_Lp ((a1 + b1),M,k)

then ( a1 a.e.= a,M & b1 a.e.= b,M ) by A2, A3, A4, A5, Th37;

hence z = a.e-eq-class_Lp ((a1 + b1),M,k) by Th42, LPSPACE1:31; :: thesis: verum

A6: for A, B being Element of CosetSet (M,k) holds S

reconsider f = f as BinOp of (CosetSet (M,k)) ;

take f ; :: thesis: for A, B being Element of CosetSet (M,k)

for a, b being PartFunc of X,REAL st a in A & b in B holds

f . (A,B) = a.e-eq-class_Lp ((a + b),M,k)

let A, B be Element of CosetSet (M,k); :: thesis: for a, b being PartFunc of X,REAL st a in A & b in B holds

f . (A,B) = a.e-eq-class_Lp ((a + b),M,k)

let a, b be PartFunc of X,REAL; :: thesis: ( a in A & b in B implies f . (A,B) = a.e-eq-class_Lp ((a + b),M,k) )

assume ( a in A & b in B ) ; :: thesis: f . (A,B) = a.e-eq-class_Lp ((a + b),M,k)

hence f . (A,B) = a.e-eq-class_Lp ((a + b),M,k) by A6; :: thesis: verum