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

per cases ;

suppose k in dom d ; :: thesis:

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

end;

suppose not k in dom d ; :: thesis:

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

end;

end;