let e1, e2 be Series of (n + 1),L; :: thesis: ( ( for b being bag of n + 1 holds
( ( b . n <> 0 implies e1 . b = 0. L ) & ( b . n = 0 implies e1 . b = p . ((0,n) -cut b) ) ) ) & ( for b being bag of n + 1 holds
( ( b . n <> 0 implies e2 . b = 0. L ) & ( b . n = 0 implies e2 . b = p . ((0,n) -cut b) ) ) ) implies e1 = e2 )
assume that
A6: for b being bag of n + 1 holds
( ( b . n <> 0 implies e1 . b = 0. L ) & ( b . n = 0 implies e1 . b = p . ((0,n) -cut b) ) ) and
A7: for b being bag of n + 1 holds
( ( b . n <> 0 implies e2 . b = 0. L ) & ( b . n = 0 implies e2 . b = p . ((0,n) -cut b) ) ) ; :: thesis: e1 = e2

now :: thesis: for b being Element of Bags (n + 1) holds e1 . b = e2 . b

let b be Element of Bags (n + 1); :: thesis: e1 . b = e2 . b
( b . n = 0 or b . n <> 0 ) ;
then ( ( e1 . b = 0. L & 0. L = e2 . b ) or ( e1 . b = p . ((0,n) -cut b) & p . ((0,n) -cut b) = e2 . b ) ) by A6, A7;
hence e1 . b = e2 . b ; :: thesis: verum

end;

hence e1 = e2 ; :: thesis: verum