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 A1: x in (f (#) (f (#) f)) " {0 } ; :: thesis: x in f " {0 }
then (f (#) (f (#) f)) . x in {0 } by FUNCT_1:def 13;
then (f (#) (f (#) f)) . x = 0 by TARSKI:def 1;
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 ( f . x = 0 or f . x = 0 or f . x = 0 ) by XCMPLX_1:6;
then A2: f . x in {0 } by TARSKI:def 1;
x in dom (f (#) (f (#) f)) by A1, FUNCT_1:def 13;
then x in (dom f) /\ (dom (f (#) f)) by VALUED_1:def 4;
then x in dom f by XBOOLE_0:def 4;
hence x in f " {0 } by A2, 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 (#) f)) " {0 } )
assume A3: x in f " {0 } ; :: thesis: x in (f (#) (f (#) f)) " {0 }
then f . x in {0 } by FUNCT_1:def 13;
then A4: f . x = 0 by TARSKI:def 1;
x in (dom f) /\ (dom f) by A3, FUNCT_1:def 13;
then x in (dom (f (#) f)) /\ (dom f) by VALUED_1:def 4;
then A5: 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 A4
.= 0 by A4 ;
then (f (#) (f (#) f)) . x in {0 } by TARSKI:def 1;
hence x in (f (#) (f (#) f)) " {0 } by A5, FUNCT_1:def 13; :: thesis: verum