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;