let C be non empty set ; 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; (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}))
XBOOLE_0:def 10 ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0})) c= (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0})
thus
((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0})) c= (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0})
verumproof
let x be
object ;
TARSKI:def 3 ( 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}))
;
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;
verum
end;