let i, j, n be Nat; :: thesis: for a, b being bag of n holds i,j -cut (a + b) = (i,j -cut a) + (i,j -cut b)
let a, b be bag of n; :: thesis: i,j -cut (a + b) = (i,j -cut a) + (i,j -cut b)
set CUTAB = i,j -cut (a + b);
set CUTA = i,j -cut a;
set CUTB = i,j -cut b;

now

let x be set ; :: thesis: ( x in j -' i implies (i,j -cut (a + b)) . x = ((i,j -cut a) + (i,j -cut b)) . x )
assume A1: x in j -' i ; :: thesis: (i,j -cut (a + b)) . x = ((i,j -cut a) + (i,j -cut b)) . x
j -' i = { k where k is Element of NAT : k < j -' i } by AXIOMS:30;
then ex k being Element of NAT st
( k = x & k < j -' i ) by A1;
then reconsider x9 = x as Element of NAT ;
(i,j -cut (a + b)) . x = (a + b) . (i + x9) by A1, Def1;
then A2: (i,j -cut (a + b)) . x = (a . (i + x9)) + (b . (i + x9)) by PRE_POLY:def 5;
A3: (i,j -cut a) . x = a . (i + x9) by A1, Def1;
(i,j -cut b) . x = b . (i + x9) by A1, Def1;
hence (i,j -cut (a + b)) . x = ((i,j -cut a) + (i,j -cut b)) . x by A2, A3, PRE_POLY:def 5; :: thesis: verum

end;

hence i,j -cut (a + b) = (i,j -cut a) + (i,j -cut b) by PBOOLE:3; :: thesis: verum