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;
set h = f + g;
A1: rng (f + g) c= COMPLEX by MEMBERED:1;
dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def 1
.= the carrier of X /\ (dom g) by PARTFUN1:def 2
.= the carrier of X /\ the carrier of X by PARTFUN1:def 2 ;
then reconsider h = f + g as Function of the carrier of X,COMPLEX by A1, FUNCT_2:2;
( dom f = the carrier of X & dom g = the carrier of X & dom h = the carrier of X ) by FUNCT_2:def 1;
then A2: ( 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 A3: ( x in the carrier of X & f . x = 0 & g . x = 0 ) by PRE_POLY:def 7;
then (f + g) . x = (f . x) + (g . x) by VALUED_1:1
.= 0 by A3 ;
then A4: ( x in the carrier of X & (f + g) . x = 0 ) by A3;
not x in support (f + g) by A4, PRE_POLY:def 7;
hence x in the carrier of X \ (support (f + g)) by A4, 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 A2, 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 A2, XBOOLE_1:28;
hence support (f + g) c= (support f) \/ (support g) by A2, XBOOLE_1:28; :: thesis: verum