let n be set ; :: thesis: for d, b being bag of n st ( for k being object st k in n holds
d . k <= b . k ) holds
d divides b
let d, b be bag of n; :: thesis: ( ( for k being object st k in n holds
d . k <= b . k ) implies d divides b )
assume A1: for k being object st k in n holds
d . k <= b . k ; :: thesis: d divides b
let k be object ; :: according to PRE_POLY:def 11 :: thesis: d . k <= b . k

per cases ( k in dom d or not k in dom d ) ;

suppose k in dom d ; :: thesis: d . k <= b . k

then k in n ;
hence d . k <= b . k by A1; :: thesis: verum

end;

suppose not k in dom d ; :: thesis: d . k <= b . k

hence d . k <= b . k by FUNCT_1:def 2; :: thesis: verum

end;

end;