let D be non empty set ; :: thesis: for F being PartFunc of D,REAL
for r being Real st r < 0 holds
(abs F) " {r} = {}
let F be PartFunc of D,REAL ; :: thesis: for r being Real st r < 0 holds
(abs F) " {r} = {}
let r be Real; :: thesis: ( r < 0 implies (abs F) " {r} = {} )
assume A1: r < 0 ; :: thesis: (abs F) " {r} = {}
assume A2: (abs F) " {r} <> {} ; :: thesis: contradiction
consider x being Element of (abs F) " {r};
reconsider x = x as Element of D by A2, TARSKI:def 3;
( x in dom (abs F) & (abs F) . x in {r} ) by A2, FUNCT_1:def 13;
then abs (F . x) in {r} by VALUED_1:18;
then abs (F . x) = r by TARSKI:def 1;
hence contradiction by A1, COMPLEX1:132; :: thesis: verum