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;

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

hence
(i,j) -cut (a + b) = ((i,j) -cut a) + ((i,j) -cut b)
by PBOOLE:3; :: thesis: verum((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;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