let M be non empty set ; :: thesis: for V being ComplexNormSpace
for f1 being PartFunc of M,COMPLEX
for f2 being PartFunc of M,the carrier of V holds (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)}) = ((dom f1) \ (f1 " {0 })) /\ ((dom f2) \ (f2 " {(0. V)}))
let V be ComplexNormSpace; :: thesis: for f1 being PartFunc of M,COMPLEX
for f2 being PartFunc of M,the carrier of V holds (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)}) = ((dom f1) \ (f1 " {0 })) /\ ((dom f2) \ (f2 " {(0. V)}))
let f1 be PartFunc of M,COMPLEX ; :: thesis: for f2 being PartFunc of M,the carrier of V holds (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)}) = ((dom f1) \ (f1 " {0 })) /\ ((dom f2) \ (f2 " {(0. V)}))
let f2 be PartFunc of M,the carrier of V; :: thesis: (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)}) = ((dom f1) \ (f1 " {0 })) /\ ((dom f2) \ (f2 " {(0. V)}))
thus (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)}) c= ((dom f1) \ (f1 " {0 })) /\ ((dom f2) \ (f2 " {(0. V)})) :: according to XBOOLE_0:def 10 :: thesis: ((dom f1) \ (f1 " {0 })) /\ ((dom f2) \ (f2 " {(0. V)})) c= (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)})

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)}) or x in ((dom f1) \ (f1 " {0 })) /\ ((dom f2) \ (f2 " {(0. V)})) )
assume A1: x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)}) ; :: thesis: x in ((dom f1) \ (f1 " {0 })) /\ ((dom f2) \ (f2 " {(0. V)}))
then reconsider x1 = x as Element of M ;
A2: x in dom (f1 (#) f2) by A1, XBOOLE_0:def 5;
then A3: x1 in (dom f1) /\ (dom f2) by Def3;
not x in (f1 (#) f2) " {(0. V)} by A1, XBOOLE_0:def 5;
then not (f1 (#) f2) /. x1 in {(0. V)} by A2, PARTFUN2:44;
then (f1 (#) f2) /. x1 <> 0. V by TARSKI:def 1;
then A4: (f1 /. x1) * (f2 /. x1) <> 0. V by A2, Def3;
then f1 /. x1 <> 0c by CLVECT_1:2;
then A5: not f1 /. x1 in {0 } by TARSKI:def 1;
f2 /. x1 <> 0. V by A4, CLVECT_1:2;
then not f2 /. x1 in {(0. V)} by TARSKI:def 1;
then A6: not x1 in f2 " {(0. V)} by PARTFUN2:44;
x1 in dom f2 by A3, XBOOLE_0:def 4;
then A7: x in (dom f2) \ (f2 " {(0. V)}) by A6, XBOOLE_0:def 5;
x1 in dom f1 by A3, XBOOLE_0:def 4;
then not f1 . x1 in {0 } by A5, PARTFUN1:def 8;
then A8: not x1 in f1 " {0 } by FUNCT_1:def 13;
x1 in dom f1 by A3, XBOOLE_0:def 4;
then x in (dom f1) \ (f1 " {0 }) by A8, XBOOLE_0:def 5;
hence x in ((dom f1) \ (f1 " {0 })) /\ ((dom f2) \ (f2 " {(0. V)})) by A7, XBOOLE_0:def 4; :: thesis: verum

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in ((dom f1) \ (f1 " {0 })) /\ ((dom f2) \ (f2 " {(0. V)})) or x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)}) )
assume A9: x in ((dom f1) \ (f1 " {0 })) /\ ((dom f2) \ (f2 " {(0. V)})) ; :: thesis: x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)})
then reconsider x1 = x as Element of M ;
A10: x in (dom f1) \ (f1 " {0 }) by A9, XBOOLE_0:def 4;
then A11: x in dom f1 by XBOOLE_0:def 5;
not x in f1 " {0 } by A10, XBOOLE_0:def 5;
then not f1 . x1 in {0 } by A11, FUNCT_1:def 13;
then f1 . x1 <> 0 by TARSKI:def 1;
then A12: f1 /. x1 <> 0 by A11, PARTFUN1:def 8;
A13: x in (dom f2) \ (f2 " {(0. V)}) by A9, XBOOLE_0:def 4;
then A14: x in dom f2 by XBOOLE_0:def 5;
then x1 in (dom f1) /\ (dom f2) by A11, XBOOLE_0:def 4;
then A15: x1 in dom (f1 (#) f2) by Def3;
not x in f2 " {(0. V)} by A13, XBOOLE_0:def 5;
then not f2 /. x1 in {(0. V)} by A14, PARTFUN2:44;
then f2 /. x1 <> 0. V by TARSKI:def 1;
then (f1 /. x1) * (f2 /. x1) <> 0. V by A12, CLVECT_1:3;
then (f1 (#) f2) /. x1 <> 0. V by A15, Def3;
then not (f1 (#) f2) /. x1 in {(0. V)} by TARSKI:def 1;
then not x in (f1 (#) f2) " {(0. V)} by PARTFUN2:44;
hence x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)}) by A15, XBOOLE_0:def 5; :: thesis: verum

end;