let i, j, n be Element of NAT ; :: thesis: for a, b being bag of holds i,j -cut (a + b) = (i,j -cut a) + (i,j -cut b)
let a, b be bag of ; :: 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 consider k being Element of NAT such that
A2: ( k = x & k < j -' i ) by A1;
reconsider x' = x as Element of NAT by A2;
(i,j -cut (a + b)) . x = (a + b) . (i + x') by A1, Def1;
then A3: (i,j -cut (a + b)) . x = (a . (i + x')) + (b . (i + x')) by POLYNOM1:def 5;
( (i,j -cut a) . x = a . (i + x') & (i,j -cut b) . x = b . (i + x') ) by A1, Def1;
hence (i,j -cut (a + b)) . x = ((i,j -cut a) + (i,j -cut b)) . x by A3, POLYNOM1:def 5; :: thesis: verum

end;

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