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 set ; :: 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 x' = x as Real ;
A2: ( x' in dom (f (#) f) & (f (#) f) . x' in {0 } ) by A1, FUNCT_1:def 13;
then A3: x' in (dom f) /\ (dom f) by VALUED_1:def 4;
0 = (f (#) f) . x' by A2, TARSKI:def 1
.= (f . x') * (f . x') by VALUED_1:5 ;
then f . x' = 0 ;
then f . x' in {0 } by TARSKI:def 1;
hence x in f " {0 } by 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 (f (#) f) " {0 } )
assume A4: x in f " {0 } ; :: thesis: x in (f (#) f) " {0 }
then reconsider x' = x as Real ;
A5: ( x' in dom f & f . x' in {0 } ) by A4, FUNCT_1:def 13;
x' in (dom f) /\ (dom f) by A4, FUNCT_1:def 13;
then A6: x' in dom (f (#) f) by VALUED_1:def 4;
0 = f . x' by A5, TARSKI:def 1;
then (f . x') * (f . x') = 0 ;
then (f (#) f) . x' = 0 by VALUED_1:5;
then (f (#) f) . x' in {0 } by TARSKI:def 1;
hence x in (f (#) f) " {0 } by A6, FUNCT_1:def 13; :: thesis: verum