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 object ; :: 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 A1: x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) ; :: thesis: x in ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0}))
then not x in (f1 (#) f2) " {0} by XBOOLE_0:def 5;
then not (f1 (#) f2) . x in {0} by A1, FUNCT_1:def 7;
then (f1 (#) f2) . x <> 0 by TARSKI:def 1;
then A2: (f1 . x) * (f2 . x) <> 0 by VALUED_1:5;
then f2 . x <> 0 ;
then not f2 . x in {0} by TARSKI:def 1;
then A3: not x in f2 " {0} by FUNCT_1:def 7;
x in dom (f1 (#) f2) by A1;
then A4: x in (dom f1) /\ (dom f2) by VALUED_1:def 4;
then x in dom f2 by XBOOLE_0:def 4;
then A5: x in (dom f2) \ (f2 " {0}) by A3, XBOOLE_0:def 5;
f1 . x <> 0 by A2;
then not f1 . x in {0} by TARSKI:def 1;
then A6: not x in f1 " {0} by FUNCT_1:def 7;
x in dom f1 by A4, XBOOLE_0:def 4;
then x in (dom f1) \ (f1 " {0}) by A6, XBOOLE_0:def 5;
hence x in ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0})) by A5, 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 object ; :: 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 A7: x in ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0})) ; :: thesis: x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0})
then x in (dom f2) \ (f2 " {0}) by XBOOLE_0:def 4;
then not x in f2 " {0} by XBOOLE_0:def 5;
then not f2 . x in {0} by A7, FUNCT_1:def 7;
then A8: f2 . x <> 0 by TARSKI:def 1;
A9: x in (dom f1) \ (f1 " {0}) by A7, XBOOLE_0:def 4;
then not x in f1 " {0} by XBOOLE_0:def 5;
then not f1 . x in {0} by A9, FUNCT_1:def 7;
then f1 . x <> 0 by TARSKI:def 1;
then (f1 . x) * (f2 . x) <> 0 by A8;
then (f1 (#) f2) . x <> 0 by VALUED_1:5;
then not (f1 (#) f2) . x in {0} by TARSKI:def 1;
then A10: not x in (f1 (#) f2) " {0} by FUNCT_1:def 7;
x in (dom f1) /\ (dom f2) by A7, A9, XBOOLE_0:def 4;
then x in dom (f1 (#) f2) by VALUED_1:def 4;
hence x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) by A10, XBOOLE_0:def 5; :: thesis: verum
end;