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
now :: thesis: for x being Point of (Pre-Lp-Space (M,k)) holds N1 . x = N2 . x
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 A4;
hence N1 . x = N2 . x by Th52; :: thesis: verum
end;
hence N1 = N2 by FUNCT_2:63; :: thesis: verum