let i, j, n be Nat; 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; (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 for x being object st x in j -' i holds
((i,j) -cut (a + b)) . x = (((i,j) -cut a) + ((i,j) -cut b)) . xlet x be
object ;
( 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
;
((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;
verum end;
hence
(i,j) -cut (a + b) = ((i,j) -cut a) + ((i,j) -cut b)
by PBOOLE:3; verum