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 2;

now :: thesis: for k being object holds ((i,j) -cut (EmptyBag n)) . k <= (EmptyBag (j -' i)) . k

let k be object ; :: 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 Nat : x < j -' i } by AXIOMS:4;
then ex x being Nat st
( k = x & x < j -' i ) by A1, A2;
then reconsider k9 = k as Element of NAT by ORDINAL1:def 12;
((i,j) -cut (EmptyBag n)) . k = (EmptyBag n) . (i + k9) by A2, Def1
.= 0 by PBOOLE:5 ;
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 2; :: 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