let n be set ; :: thesis: for d, b being bag of st ( for k being set st k in n holds
d . k <= b . k ) holds
d divides b
let d, b be bag of ; :: thesis: ( ( for k being set st k in n holds
d . k <= b . k ) implies d divides b )
assume A1: for k being set st k in n holds
d . k <= b . k ; :: thesis: d divides b
let k be set ; :: according to POLYNOM1:def 13 :: 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 by PARTFUN1:def 4;
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 4; :: thesis: verum

end;

end;