let N1, N2 be Function of the carrier of (Pre-L-Space M), REAL ; :: thesis: ( ( for x being Point of (Pre-L-Space M) ex f being PartFunc of X, REAL st
( f in x & N1 . x = Integral M,(abs f) ) ) & ( for x being Point of (Pre-L-Space M) ex f being PartFunc of X, REAL st
( f in x & N2 . x = Integral M,(abs f) ) ) implies N1 = N2 )
assume A1: ( ( for x being Point of (Pre-L-Space M) ex f being PartFunc of X, REAL st
( f in x & N1 . x = Integral M,(abs f) ) ) & ( for x being Point of (Pre-L-Space M) ex g being PartFunc of X, REAL st
( g in x & N2 . x = Integral M,(abs g) ) ) ) ; :: thesis: N1 = N2

now

let x be Point of (Pre-L-Space M); :: thesis: N1 . x = N2 . x
( ex f being PartFunc of X, REAL st
( f in x & N1 . x = Integral M,(abs f) ) & ex g being PartFunc of X, REAL st
( g in x & N2 . x = Integral M,(abs g) ) ) by A1;
hence N1 . x = N2 . x by Lm17; :: thesis: verum

end;

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