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 :: thesis: for x being object st x in j -' i holds
((i,j) -cut (a + b)) . x = (((i,j) -cut a) + ((i,j) -cut b)) . x

let x be object ; :: 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 Nat : k < j -' i } by AXIOMS:4;
then ex k being Nat st
( k = x & k < j -' i ) by A1;
then reconsider x9 = x as Element of NAT by ORDINAL1:def 12;
((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