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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (0 (#) F) " {0} or x in dom F )
assume A1: x in (0 (#) F) " {0} ; :: thesis: x in dom F
then reconsider d = x as Element of D ;
d in dom (0 (#) F) by A1, FUNCT_1:def 7;
hence x in dom F by VALUED_1:def 5; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom F or x in (0 (#) F) " {0} )
assume A2: x in dom F ; :: thesis: x in (0 (#) F) " {0}
then reconsider d = x as Element of D ;
A3: d in dom (0 (#) F) by A2, VALUED_1:def 5;
then (0 (#) F) . d = 0 * (F . d) by VALUED_1:def 5
.= 0 ;
then (0 (#) F) . d in {0} by TARSKI:def 1;
hence x in (0 (#) F) " {0} by A3, FUNCT_1:def 7; :: thesis: verum