let i, j, n be Nat; :: thesis: i,j -cut (EmptyBag n) = EmptyBag (j -' i)
set CUT1 = i,j -cut (EmptyBag n);
A1: dom (i,j -cut (EmptyBag n)) = j -' i by PARTFUN1:def 4;

now

let k be set ; :: thesis: (i,j -cut (EmptyBag n)) . b₁ <= (EmptyBag (j -' i)) . b₁

per cases ( k in dom (i,j -cut (EmptyBag n)) or not k in dom (i,j -cut (EmptyBag n)) ) ;

suppose A2: k in dom (i,j -cut (EmptyBag n)) ; :: thesis: (i,j -cut (EmptyBag n)) . b₁ <= (EmptyBag (j -' i)) . b₁

j -' i = { x where x is Element of NAT : x < j -' i } by AXIOMS:30;
then ex x being Element of NAT st
( k = x & x < j -' i ) by A1, A2;
then reconsider k9 = k as Element of NAT ;
(i,j -cut (EmptyBag n)) . k = (EmptyBag n) . (i + k9) by A1, A2, Def1
.= 0 by PRE_POLY:52 ;
hence (i,j -cut (EmptyBag n)) . k <= (EmptyBag (j -' i)) . k ; :: thesis: verum

end;

suppose not k in dom (i,j -cut (EmptyBag n)) ; :: thesis: (i,j -cut (EmptyBag n)) . b₁ <= (EmptyBag (j -' i)) . b₁

hence (i,j -cut (EmptyBag n)) . k <= (EmptyBag (j -' i)) . k by FUNCT_1:def 4; :: thesis: verum

end;

end;

end;

then i,j -cut (EmptyBag n) divides EmptyBag (j -' i) by PRE_POLY:def 11;
hence i,j -cut (EmptyBag n) = EmptyBag (j -' i) by PRE_POLY:58; :: thesis: verum