let I, J be set ; :: thesis: for m being bag of I holds support (m | J) = J /\ (support m)
let m be bag of I; :: thesis: support (m | J) = J /\ (support m)
set f = m | J;
thus support (m | J) c= J /\ (support m) :: according to XBOOLE_0:def 10 :: thesis: J /\ (support m) c= support (m | J)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support (m | J) or x in J /\ (support m) )
assume x in support (m | J) ; :: thesis: x in J /\ (support m)
then A3: (m | J) . x <> 0 by PRE_POLY:def 7;
then A4: ( x in dom (m | J) & dom (m | J) = I ) by PARTFUN1:def 2, FUNCT_1:def 2;
then A5: x in J by BAR, A3;
then (m | J) . x = m . x by BAR, A4;
then x in support m by A3, PRE_POLY:def 7;
hence x in J /\ (support m) by A5, XBOOLE_0:def 4; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in J /\ (support m) or x in support (m | J) )
assume x in J /\ (support m) ; :: thesis: x in support (m | J)
then A1: ( x in J & x in support m ) by XBOOLE_0:def 4;
then A2: m . x <> 0 by PRE_POLY:def 7;
then ( x in dom m & dom m = I ) by PARTFUN1:def 2, FUNCT_1:def 2;
then (m | J) . x = m . x by A1, BAR;
hence x in support (m | J) by A2, PRE_POLY:def 7; :: thesis: verum