let f be PartFunc of REAL,REAL; :: thesis: (f (#) f) " {0} = f " {0}
thus (f (#) f) " {0} c= f " {0} :: according to XBOOLE_0:def 10 :: thesis: f " {0} c= (f (#) f) " {0}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (f (#) f) " {0} or x in f " {0} )
assume A1: x in (f (#) f) " {0} ; :: thesis: x in f " {0}
then reconsider x9 = x as Real ;
(f (#) f) . x9 in {0} by A1, FUNCT_1:def 7;
then 0 = (f (#) f) . x9 by TARSKI:def 1
.= (f . x9) * (f . x9) by VALUED_1:5 ;
then f . x9 = 0 ;
then A2: f . x9 in {0} by TARSKI:def 1;
x9 in dom (f (#) f) by A1, FUNCT_1:def 7;
then x9 in (dom f) /\ (dom f) by VALUED_1:def 4;
hence x in f " {0} by A2, 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 (f (#) f) " {0} )
assume A3: x in f " {0} ; :: thesis: x in (f (#) f) " {0}
then reconsider x9 = x as Real ;
f . x9 in {0} by A3, FUNCT_1:def 7;
then 0 = f . x9 by TARSKI:def 1;
then (f . x9) * (f . x9) = 0 ;
then (f (#) f) . x9 = 0 by VALUED_1:5;
then A4: (f (#) f) . x9 in {0} by TARSKI:def 1;
x9 in (dom f) /\ (dom f) by A3, FUNCT_1:def 7;
then x9 in dom (f (#) f) by VALUED_1:def 4;
hence x in (f (#) f) " {0} by A4, FUNCT_1:def 7; :: thesis: verum