let X be set ; :: thesis: for f being Function holds support ((EmptyBag X) +* f) = support f
let f be Function; :: thesis: support ((EmptyBag X) +* f) = support f
set F = (EmptyBag X) +* f;
support ((EmptyBag X) +* f) c= (support (EmptyBag X)) \/ (support f) by GLIB_004:1;
hence support ((EmptyBag X) +* f) c= support f ; :: according to XBOOLE_0:def 10 :: thesis: support f c= support ((EmptyBag X) +* f)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support f or x in support ((EmptyBag X) +* f) )
assume A1: x in support f ; :: thesis: x in support ((EmptyBag X) +* f)
then A2: f . x <> 0 by PRE_POLY:def 7;
support f c= dom f by PRE_POLY:37;
then ((EmptyBag X) +* f) . x = f . x by A1, FUNCT_4:13;
hence x in support ((EmptyBag X) +* f) by A2, PRE_POLY:def 7; :: thesis: verum