let N1, N2 be Function of the carrier of (Pre-L-CSpace M),REAL; ( ( for x being Point of (Pre-L-CSpace M) ex f being PartFunc of X,COMPLEX st
( f in x & N1 . x = Integral (M,(abs f)) ) ) & ( for x being Point of (Pre-L-CSpace M) ex f being PartFunc of X,COMPLEX st
( f in x & N2 . x = Integral (M,(abs f)) ) ) implies N1 = N2 )
assume A1:
( ( for x being Point of (Pre-L-CSpace M) ex f being PartFunc of X,COMPLEX st
( f in x & N1 . x = Integral (M,(abs f)) ) ) & ( for x being Point of (Pre-L-CSpace M) ex g being PartFunc of X,COMPLEX st
( g in x & N2 . x = Integral (M,(abs g)) ) ) )
; N1 = N2
hence
N1 = N2
by FUNCT_2:def 8; verum