let i, j be set ; :: thesis: for b1, b2 being bag of j
for b19, b29 being bag of i st b19 = b1 | i & b29 = b2 | i & b1 divides b2 holds
b19 divides b29
let b1, b2 be bag of j; :: thesis: for b19, b29 being bag of i st b19 = b1 | i & b29 = b2 | i & b1 divides b2 holds
b19 divides b29
let b19, b29 be bag of i; :: thesis: ( b19 = b1 | i & b29 = b2 | i & b1 divides b2 implies b19 divides b29 )
assume that
A1: ( b19 = b1 | i & b29 = b2 | i ) and
A2: b1 divides b2 ; :: thesis: b19 divides b29

now :: thesis: for k being object holds b19 . k <= b29 . k

let k be object ; :: thesis: b19 . b₁ <= b29 . b₁
A3: dom b19 = i by PARTFUN1:def 2
.= dom b29 by PARTFUN1:def 2 ;

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

suppose A4: not k in dom b19 ; :: thesis: b19 . b₁ <= b29 . b₁

then b19 . k = {} by FUNCT_1:def 2
.= b29 . k by A3, A4, FUNCT_1:def 2 ;
hence b19 . k <= b29 . k ; :: thesis: verum

end;

suppose k in dom b19 ; :: thesis: b19 . b₁ <= b29 . b₁

then ( b19 . k = b1 . k & b29 . k = b2 . k ) by A1, A3, FUNCT_1:47;
hence b19 . k <= b29 . k by A2, PRE_POLY:def 11; :: thesis: verum

end;

end;

end;

hence b19 divides b29 by PRE_POLY:def 11; :: thesis: verum