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} = {}
set x = the Element of (abs F) " {r};
assume A2: (abs F) " {r} <> {} ; :: thesis: contradiction
then reconsider x = the Element of (abs F) " {r} as Element of D by TARSKI:def 3;
(abs F) . x in {r} by A2, FUNCT_1:def 7;
then |.(F . x).| in {r} by VALUED_1:18;
then |.(F . x).| = r by TARSKI:def 1;
hence contradiction by A1, COMPLEX1:46; :: thesis: verum