let X be non empty TopSpace; :: thesis: for f, g being Function of the carrier of X,COMPLEX holds support (f (#) g) c= (support f) \/ (support g)
let f, g be Function of the carrier of X,COMPLEX; :: thesis: support (f (#) g) c= (support f) \/ (support g)
set CX = the carrier of X;
reconsider h = f (#) g as Function of the carrier of X,COMPLEX ;
( dom f = the carrier of X & dom g = the carrier of X & dom h = the carrier of X ) by FUNCT_2:def 1;
then A1: ( support f c= the carrier of X & support g c= the carrier of X & support h c= the carrier of X ) by PRE_POLY:37;

now :: thesis: for x being object st x in ( the carrier of X \ (support f)) /\ ( the carrier of X \ (support g)) holds
x in the carrier of X \ (support (f (#) g))

let x be object ; :: thesis: ( x in ( the carrier of X \ (support f)) /\ ( the carrier of X \ (support g)) implies x in the carrier of X \ (support (f (#) g)) )
assume x in ( the carrier of X \ (support f)) /\ ( the carrier of X \ (support g)) ; :: thesis: x in the carrier of X \ (support (f (#) g))
then ( x in the carrier of X \ (support f) & x in the carrier of X \ (support g) ) by XBOOLE_0:def 4;
then ( x in the carrier of X & not x in support f & x in the carrier of X & not x in support g ) by XBOOLE_0:def 5;
then A2: ( x in the carrier of X & f . x = 0 & g . x = 0 ) by PRE_POLY:def 7;
(f (#) g) . x = 0 * 0 by A2, VALUED_1:5;
then A3: ( x in the carrier of X & (f (#) g) . x = 0 ) by A2;
not x in support (f (#) g) by A3, PRE_POLY:def 7;
hence x in the carrier of X \ (support (f (#) g)) by A3, XBOOLE_0:def 5; :: thesis: verum

end;

then ( the carrier of X \ (support f)) /\ ( the carrier of X \ (support g)) c= the carrier of X \ (support (f (#) g)) ;
then the carrier of X \ ((support f) \/ (support g)) c= the carrier of X \ (support (f (#) g)) by XBOOLE_1:53;
then the carrier of X \ ( the carrier of X \ (support (f (#) g))) c= the carrier of X \ ( the carrier of X \ ((support f) \/ (support g))) by XBOOLE_1:34;
then the carrier of X /\ (support (f (#) g)) c= the carrier of X \ ( the carrier of X \ ((support f) \/ (support g))) by XBOOLE_1:48;
then the carrier of X /\ (support (f (#) g)) c= the carrier of X /\ ((support f) \/ (support g)) by XBOOLE_1:48;
then support (f (#) g) c= the carrier of X /\ ((support f) \/ (support g)) by A1, XBOOLE_1:28;
then support (f (#) g) c= ( the carrier of X /\ (support f)) \/ ( the carrier of X /\ (support g)) by XBOOLE_1:23;
then support (f (#) g) c= (support f) \/ ( the carrier of X /\ (support g)) by A1, XBOOLE_1:28;
hence support (f (#) g) c= (support f) \/ (support g) by A1, XBOOLE_1:28; :: thesis: verum