let n be Nat; :: thesis: for b being bag of n + 1 holds b = ((0,n) -cut b) bag_extend (b . n)
let b be bag of n + 1; :: thesis: b = ((0,n) -cut b) bag_extend (b . n)
set C = (0,n) -cut b;
set B = ((0,n) -cut b) bag_extend (b . n);
A1: n -' 0 = n by NAT_D:40;
then A2: ( (((0,n) -cut b) bag_extend (b . n)) | n = (0,n) -cut b & (((0,n) -cut b) bag_extend (b . n)) . n = b . n ) by HILBASIS:def 1;
A3: (0,n) -cut b = b | n by Th3, NAT_1:11;
A4: ( dom b = n + 1 & n + 1 = dom (((0,n) -cut b) bag_extend (b . n)) ) by A1, PARTFUN1:def 2;
for x being object st x in n + 1 holds
(((0,n) -cut b) bag_extend (b . n)) . x = b . x

proof

let x be object ; :: thesis: ( x in n + 1 implies (((0,n) -cut b) bag_extend (b . n)) . x = b . x )
assume x in n + 1 ; :: thesis: (((0,n) -cut b) bag_extend (b . n)) . x = b . x
then x in Segm (n + 1) ;
then x in (Segm n) \/ {n} by AFINSQ_1:2;
then ( x in n or x = n ) by ZFMISC_1:136;
then ( ( (((0,n) -cut b) bag_extend (b . n)) . x = ((0,n) -cut b) . x & ((0,n) -cut b) . x = b . x ) or (((0,n) -cut b) bag_extend (b . n)) . x = b . x ) by FUNCT_1:49, A2, A3;
hence (((0,n) -cut b) bag_extend (b . n)) . x = b . x ; :: thesis: verum

end;

hence b = ((0,n) -cut b) bag_extend (b . n) by FUNCT_1:2, A4; :: thesis: verum