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 A5: ( ( 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 :: thesis: for x being Point of (Pre-L-Space M) holds N1 . x = N2 . x

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 A5;
hence N1 . x = N2 . x by Th48; :: thesis: verum

end;

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