let N1, N2 be Function of the carrier of (Pre-Lp-Space (M,k)),REAL; :: thesis: ( ( for x being Point of (Pre-Lp-Space (M,k)) ex f being PartFunc of X,REAL st

( f in x & ex r being Real st

( r = Integral (M,((abs f) to_power k)) & N1 . x = r to_power (1 / k) ) ) ) & ( for x being Point of (Pre-Lp-Space (M,k)) ex f being PartFunc of X,REAL st

( f in x & ex r being Real st

( r = Integral (M,((abs f) to_power k)) & N2 . x = r to_power (1 / k) ) ) ) implies N1 = N2 )

assume A4: ( ( for x being Point of (Pre-Lp-Space (M,k)) ex f being PartFunc of X,REAL st

( f in x & ex r1 being Real st

( r1 = Integral (M,((abs f) to_power k)) & N1 . x = r1 to_power (1 / k) ) ) ) & ( for x being Point of (Pre-Lp-Space (M,k)) ex g being PartFunc of X,REAL st

( g in x & ex r2 being Real st

( r2 = Integral (M,((abs g) to_power k)) & N2 . x = r2 to_power (1 / k) ) ) ) ) ; :: thesis: N1 = N2

( f in x & ex r being Real st

( r = Integral (M,((abs f) to_power k)) & N1 . x = r to_power (1 / k) ) ) ) & ( for x being Point of (Pre-Lp-Space (M,k)) ex f being PartFunc of X,REAL st

( f in x & ex r being Real st

( r = Integral (M,((abs f) to_power k)) & N2 . x = r to_power (1 / k) ) ) ) implies N1 = N2 )

assume A4: ( ( for x being Point of (Pre-Lp-Space (M,k)) ex f being PartFunc of X,REAL st

( f in x & ex r1 being Real st

( r1 = Integral (M,((abs f) to_power k)) & N1 . x = r1 to_power (1 / k) ) ) ) & ( for x being Point of (Pre-Lp-Space (M,k)) ex g being PartFunc of X,REAL st

( g in x & ex r2 being Real st

( r2 = Integral (M,((abs g) to_power k)) & N2 . x = r2 to_power (1 / k) ) ) ) ) ; :: thesis: N1 = N2

now :: thesis: for x being Point of (Pre-Lp-Space (M,k)) holds N1 . x = N2 . x

hence
N1 = N2
by FUNCT_2:63; :: thesis: verumlet x be Point of (Pre-Lp-Space (M,k)); :: thesis: N1 . x = N2 . x

( ex f being PartFunc of X,REAL st

( f in x & ex r1 being Real st

( r1 = Integral (M,((abs f) to_power k)) & N1 . x = r1 to_power (1 / k) ) ) & ex g being PartFunc of X,REAL st

( g in x & ex r2 being Real st

( r2 = Integral (M,((abs g) to_power k)) & N2 . x = r2 to_power (1 / k) ) ) ) by A4;

hence N1 . x = N2 . x by Th52; :: thesis: verum

end;( ex f being PartFunc of X,REAL st

( f in x & ex r1 being Real st

( r1 = Integral (M,((abs f) to_power k)) & N1 . x = r1 to_power (1 / k) ) ) & ex g being PartFunc of X,REAL st

( g in x & ex r2 being Real st

( r2 = Integral (M,((abs g) to_power k)) & N2 . x = r2 to_power (1 / k) ) ) ) by A4;

hence N1 . x = N2 . x by Th52; :: thesis: verum