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

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

hence
b19 divides b29
by PRE_POLY:def 11; :: thesis: verumlet k be object ; :: thesis: b19 . b_{1} <= b29 . b_{1}

A3: dom b19 = i by PARTFUN1:def 2

.= dom b29 by PARTFUN1:def 2 ;

end;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 )
;

end;

suppose A4:
not k in dom b19
; :: thesis: b19 . b_{1} <= b29 . b_{1}

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;.= b29 . k by A3, A4, FUNCT_1:def 2 ;

hence b19 . k <= b29 . k ; :: thesis: verum

suppose
k in dom b19
; :: thesis: b19 . b_{1} <= b29 . b_{1}

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;hence b19 . k <= b29 . k by A2, PRE_POLY:def 11; :: thesis: verum