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

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 A2: 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: ( ( not x in dom f or f /. x = 0. T ) & ( not x in dom g or g /. x = 0. T ) ) by Def10;
A4: (f + g) /. x = (0. T) + (0. T) by A3, A2, A1, VFUNCT_1:def 1;
not x in support (f + g) by A4, Def10;
hence x in the carrier of X \ (support (f + g)) by A2, 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 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 XBOOLE_1:28;
hence support (f + g) c= (support f) \/ (support g) by XBOOLE_1:28; :: thesis: verum