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 A1: ( ( 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

let 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 A1;
hence N1 . x = N2 . x by Lm17; :: thesis: verum

end;

hence N1 = N2 by FUNCT_2:113; :: thesis: verum