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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (f (#) (f (#) f)) " {0 } or x in f " {0 } )
assume x in (f (#) (f (#) f)) " {0 } ; :: thesis: x in f " {0 }
then ( x in dom (f (#) (f (#) f)) & (f (#) (f (#) f)) . x in {0 } ) by FUNCT_1:def 13;
then ( x in dom (f (#) (f (#) f)) & (f (#) (f (#) f)) . x = 0 ) by TARSKI:def 1;
then ZZ: ( x in (dom f) /\ (dom (f (#) f)) & (f (#) (f (#) f)) . x = 0 ) by VALUED_1:def 4;
then (f . x) * ((f (#) f) . x) = 0 by VALUED_1:5;
then ((f . x) * (f . x)) * (f . x) = 0 by VALUED_1:5;
then ( f . x = 0 or (f . x) * (f . x) = 0 ) by XCMPLX_1:6;
then Z0: ( f . x = 0 or f . x = 0 or f . x = 0 ) by XCMPLX_1:6;
Z2: x in dom f by ZZ, XBOOLE_0:def 4;
f . x in {0 } by Z0, TARSKI:def 1;
then x in f " {0 } by Z2, FUNCT_1:def 13;
hence x in f " {0 } ; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in f " {0 } or x in (f (#) (f (#) f)) " {0 } )
assume x in f " {0 } ; :: thesis: x in (f (#) (f (#) f)) " {0 }
then ZZ: ( x in dom f & f . x in {0 } ) by FUNCT_1:def 13;
then Z0: f . x = 0 by TARSKI:def 1;
x in (dom f) /\ (dom f) by ZZ;
then x in dom (f (#) f) by VALUED_1:def 4;
then x in (dom (f (#) f)) /\ (dom f) by ZZ, XBOOLE_0:def 4;
then Z2: x in dom (f (#) (f (#) f)) by VALUED_1:def 4;
(f (#) (f (#) f)) . x = (f . x) * ((f (#) f) . x) by VALUED_1:5
.= (f . x) * (f . x) by Z0
.= 0 by Z0 ;
then (f (#) (f (#) f)) . x in {0 } by TARSKI:def 1;
then x in (f (#) (f (#) f)) " {0 } by Z2, FUNCT_1:def 13;
hence x in (f (#) (f (#) f)) " {0 } ; :: thesis: verum