let C be non empty set ; :: thesis: for f1, f2 being PartFunc of C,COMPLEX holds (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) = ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0}))
let f1, f2 be PartFunc of C,COMPLEX; :: 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 A2: x in dom (f1 (#) f2) by XBOOLE_0:def 5;
reconsider x1 = x as Element of C by A1;
not x in (f1 (#) f2) " {0c} by A1, XBOOLE_0:def 5;
then not (f1 (#) f2) /. x1 in {0c} by A2, PARTFUN2:26;
then (f1 (#) f2) /. x1 <> 0c by TARSKI:def 1;
then A3: (f1 /. x1) * (f2 /. x1) <> 0c by A2, Th3;
then f2 /. x1 <> 0c ;
then not f2 /. x1 in {0c} by TARSKI:def 1;
then A4: not x1 in f2 " {0c} by PARTFUN2:26;
A5: x1 in (dom f1) /\ (dom f2) by A2, Th3;
then x1 in dom f2 by XBOOLE_0:def 4;
then A6: x in (dom f2) \ (f2 " {0c}) by A4, XBOOLE_0:def 5;
f1 /. x1 <> 0c by A3;
then not f1 /. x1 in {0c} by TARSKI:def 1;
then A7: not x1 in f1 " {0c} by PARTFUN2:26;
x1 in dom f1 by A5, XBOOLE_0:def 4;
then x in (dom f1) \ (f1 " {0c}) by A7, XBOOLE_0:def 5;
hence x in ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0})) by A6, 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 A8: x in ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0})) ; :: thesis: x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0})
then reconsider x1 = x as Element of C ;
A9: x in (dom f2) \ (f2 " {0c}) by A8, XBOOLE_0:def 4;
then A10: x in dom f2 by XBOOLE_0:def 5;
not x in f2 " {0c} by A9, XBOOLE_0:def 5;
then not f2 /. x1 in {0c} by A10, PARTFUN2:26;
then A11: f2 /. x1 <> 0c by TARSKI:def 1;
A12: x in (dom f1) \ (f1 " {0c}) by A8, XBOOLE_0:def 4;
then A13: x in dom f1 by XBOOLE_0:def 5;
then x1 in (dom f1) /\ (dom f2) by A10, XBOOLE_0:def 4;
then A14: x1 in dom (f1 (#) f2) by Th3;
not x in f1 " {0c} by A12, XBOOLE_0:def 5;
then not f1 /. x1 in {0c} by A13, PARTFUN2:26;
then f1 /. x1 <> 0c by TARSKI:def 1;
then (f1 /. x1) * (f2 /. x1) <> 0c by A11, XCMPLX_1:6;
then (f1 (#) f2) /. x1 <> 0c by A14, Th3;
then not (f1 (#) f2) /. x1 in {0c} by TARSKI:def 1;
then not x in (f1 (#) f2) " {0c} by PARTFUN2:26;
hence x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) by A14, XBOOLE_0:def 5; :: thesis: verum
end;