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 object ; :: 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 7;
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 7;
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 7; :: thesis: verum
end;
let x be object ; :: 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 7;
then A4: f . x = 0 by TARSKI:def 1;
x in (dom f) /\ (dom f) by A3, FUNCT_1:def 7;
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 7; :: thesis: verum