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

now

let k be set ; :: thesis: b1' . b₁ <= b2' . b₁
A3: dom b1' = i by PARTFUN1:def 4
.= dom b2' by PARTFUN1:def 4 ;

per cases ( not k in dom b1' or k in dom b1' ) ;

suppose A4: not k in dom b1' ; :: thesis: b1' . b₁ <= b2' . b₁

then b1' . k = {} by FUNCT_1:def 4
.= b2' . k by A3, A4, FUNCT_1:def 4 ;
hence b1' . k <= b2' . k ; :: thesis: verum

end;

suppose k in dom b1' ; :: thesis: b1' . b₁ <= b2' . b₁

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

end;

end;

end;

hence b1' divides b2' by PRE_POLY:def 11; :: thesis: verum