let X be non empty set ; :: thesis: for f being PartFunc of X,COMPLEX holds |.f.| is nonnegative

let f be PartFunc of X,COMPLEX; :: thesis: |.f.| is nonnegative

let f be PartFunc of X,COMPLEX; :: thesis: |.f.| is nonnegative

now :: thesis: for x being object st x in dom |.f.| holds

0 <= |.f.| . x

hence
|.f.| is nonnegative
by MESFUNC6:52; :: thesis: verum0 <= |.f.| . x

let x be object ; :: thesis: ( x in dom |.f.| implies 0 <= |.f.| . x )

assume x in dom |.f.| ; :: thesis: 0 <= |.f.| . x

then |.f.| . x = |.(f . x).| by VALUED_1:def 11;

hence 0 <= |.f.| . x by COMPLEX1:46; :: thesis: verum

end;assume x in dom |.f.| ; :: thesis: 0 <= |.f.| . x

then |.f.| . x = |.(f . x).| by VALUED_1:def 11;

hence 0 <= |.f.| . x by COMPLEX1:46; :: thesis: verum