let D be non empty set ; :: thesis: for F being PartFunc of D,REAL holds (abs F) " {0 } = F " {0 }
let F be PartFunc of D,REAL ; :: thesis: (abs F) " {0 } = F " {0 }
A1: dom (abs F) = dom F by VALUED_1:def 11;
thus (abs F) " {0 } c= F " {0 } :: according to XBOOLE_0:def 10 :: thesis: F " {0 } c= (abs F) " {0 }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (abs F) " {0 } or x in F " {0 } )
assume A2: x in (abs F) " {0 } ; :: thesis: x in F " {0 }
then reconsider r = x as Element of D ;
A3: ( r in dom (abs F) & (abs F) . r in {0 } ) by A2, FUNCT_1:def 13;
then abs (F . r) in {0 } by VALUED_1:18;
then abs (F . r) = 0 by TARSKI:def 1;
then F . r = 0 by ABSVALUE:7;
then F . r in {0 } by TARSKI:def 1;
hence x in F " {0 } by A1, A3, FUNCT_1:def 13; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in F " {0 } or x in (abs F) " {0 } )
assume A4: x in F " {0 } ; :: thesis: x in (abs F) " {0 }
then reconsider r = x as Element of D ;
A5: ( r in dom F & F . r in {0 } ) by A4, FUNCT_1:def 13;
then F . r = 0 by TARSKI:def 1;
then abs (F . r) = 0 by ABSVALUE:7;
then (abs F) . r = 0 by VALUED_1:18;
then (abs F) . r in {0 } by TARSKI:def 1;
hence x in (abs F) " {0 } by A1, A5, FUNCT_1:def 13; :: thesis: verum