let I, J be set ; :: thesis: for m being bag of I holds m | J divides m
let m be bag of I; :: thesis: m | J divides m
let i be object ; :: according to PRE_POLY:def 11 :: thesis: (m | J) . i <= m . i

per cases ( not i in I or i in I ) ;

suppose A1: not i in I ; :: thesis: (m | J) . i <= m . i

( dom (m | J) = I & dom m = I ) by PARTFUN1:def 2;
hence (m | J) . i <= m . i by A1, FUNCT_1:def 2; :: thesis: verum

end;

suppose A2: i in I ; :: thesis: (m | J) . i <= m . i

per cases ( i in J or not i in J ) ;

suppose i in J ; :: thesis: (m | J) . i <= m . i

hence (m | J) . i <= m . i by A2, BAR; :: thesis: verum

end;

suppose not i in J ; :: thesis: (m | J) . i <= m . i

hence (m | J) . i <= m . i by A2, BAR; :: thesis: verum

end;

end;

end;

end;