set C = CosetSet (M,k);
let f1, f2 be Function of [:REAL,(CosetSet (M,k)):],(CosetSet (M,k)); ( ( for z being Real
for A being Element of CosetSet (M,k)
for f being PartFunc of X,REAL st f in A holds
f1 . (z,A) = a.e-eq-class_Lp ((z (#) f),M,k) ) & ( for z being Real
for A being Element of CosetSet (M,k)
for f being PartFunc of X,REAL st f in A holds
f2 . (z,A) = a.e-eq-class_Lp ((z (#) f),M,k) ) implies f1 = f2 )
assume that
A6:
for z being Real
for A being Element of CosetSet (M,k)
for a being PartFunc of X,REAL st a in A holds
f1 . (z,A) = a.e-eq-class_Lp ((z (#) a),M,k)
and
A7:
for z being Real
for A being Element of CosetSet (M,k)
for a being PartFunc of X,REAL st a in A holds
f2 . (z,A) = a.e-eq-class_Lp ((z (#) a),M,k)
; f1 = f2
now for z being Element of REAL
for A being Element of CosetSet (M,k) holds f1 . (z,A) = f2 . (z,A)let z be
Element of
REAL ;
for A being Element of CosetSet (M,k) holds f1 . (z,A) = f2 . (z,A)let A be
Element of
CosetSet (
M,
k);
f1 . (z,A) = f2 . (z,A)
A in CosetSet (
M,
k)
;
then consider a1 being
PartFunc of
X,
REAL such that A8:
(
A = a.e-eq-class_Lp (
a1,
M,
k) &
a1 in Lp_Functions (
M,
k) )
;
thus f1 . (
z,
A) =
a.e-eq-class_Lp (
(z (#) a1),
M,
k)
by A6, A8, Th38
.=
f2 . (
z,
A)
by A7, A8, Th38
;
verum end;
hence
f1 = f2
by BINOP_1:2; verum