let f1, f2 be complex-valued Function; :: thesis: (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0 }) = ((dom f1) \ (f1 " {0 })) /\ ((dom f2) \ (f2 " {0 }))
thus (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0 }) c= ((dom f1) \ (f1 " {0 })) /\ ((dom f2) \ (f2 " {0 })) :: according to XBOOLE_0:def 10 :: thesis: ((dom f1) \ (f1 " {0 })) /\ ((dom f2) \ (f2 " {0 })) c= (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0 })

proof

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

end;

thus ((dom f1) \ (f1 " {0 })) /\ ((dom f2) \ (f2 " {0 })) c= (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0 }) :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in ((dom f1) \ (f1 " {0 })) /\ ((dom f2) \ (f2 " {0 })) or x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0 }) )
assume x in ((dom f1) \ (f1 " {0 })) /\ ((dom f2) \ (f2 " {0 })) ; :: thesis: x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0 })
then A2: ( x in (dom f1) \ (f1 " {0 }) & x in (dom f2) \ (f2 " {0 }) ) by XBOOLE_0:def 4;
then A3: ( x in dom f1 & not x in f1 " {0 } & x in dom f2 & not x in f2 " {0 } ) by XBOOLE_0:def 5;
then not f1 . x in {0 } by FUNCT_1:def 13;
then A4: f1 . x <> 0 by TARSKI:def 1;
not f2 . x in {0 } by A3, FUNCT_1:def 13;
then f2 . x <> 0 by TARSKI:def 1;
then A5: (f1 . x) * (f2 . x) <> 0 by A4;
x in (dom f1) /\ (dom f2) by A2, XBOOLE_0:def 4;
then A6: x in dom (f1 (#) f2) by VALUED_1:def 4;
(f1 (#) f2) . x <> 0 by A5, VALUED_1:5;
then not (f1 (#) f2) . x in {0 } by TARSKI:def 1;
then not x in (f1 (#) f2) " {0 } by FUNCT_1:def 13;
hence x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0 }) by A6, XBOOLE_0:def 5; :: thesis: verum

end;