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;

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

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

then
(i,j) -cut (EmptyBag n) divides EmptyBag (j -' i)
by PRE_POLY:def 11;let k be object ; :: thesis: ((i,j) -cut (EmptyBag n)) . b_{1} <= (EmptyBag (j -' i)) . b_{1}

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

end;

suppose A2:
k in dom ((i,j) -cut (EmptyBag n))
; :: thesis: ((i,j) -cut (EmptyBag n)) . b_{1} <= (EmptyBag (j -' i)) . b_{1}

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

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