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 object ; :: 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 ;
(abs F) . r in {0} by A2, FUNCT_1:def 7;
then |.(F . r).| in {0} by VALUED_1:18;
then |.(F . r).| = 0 by TARSKI:def 1;
then F . r = 0 by ABSVALUE:2;
then A3: F . r in {0} by TARSKI:def 1;
r in dom (abs F) by A2, FUNCT_1:def 7;
hence x in F " {0} by A1, A3, FUNCT_1:def 7; :: thesis: verum

end;

let x be object ; :: 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 ;
F . r in {0} by A4, FUNCT_1:def 7;
then F . r = 0 by TARSKI:def 1;
then |.(F . r).| = 0 by ABSVALUE:2;
then (abs F) . r = 0 by VALUED_1:18;
then A5: (abs F) . r in {0} by TARSKI:def 1;
r in dom F by A4, FUNCT_1:def 7;
hence x in (abs F) " {0} by A1, A5, FUNCT_1:def 7; :: thesis: verum