let p1, p2 be Series of n,L; :: thesis: ( ( for b' being bag of n st b divides b' holds
( p1 . b' = p . (b' -' b) & ( for b' being bag of n st not b divides b' holds
p1 . b' = 0. L ) ) ) & ( for b' being bag of n st b divides b' holds
( p2 . b' = p . (b' -' b) & ( for b' being bag of n st not b divides b' holds
p2 . b' = 0. L ) ) ) implies p1 = p2 )
assume that
A32: for b' being bag of n st b divides b' holds
( p1 . b' = p . (b' -' b) & ( for b' being bag of n st not b divides b' holds
p1 . b' = 0. L ) ) and
A33: for b' being bag of n st b divides b' holds
( p2 . b' = p . (b' -' b) & ( for b' being bag of n st not b divides b' holds
p2 . b' = 0. L ) ) ; :: thesis: p1 = p2

now

let x be Element of Bags n; :: thesis: p1 . x = p2 . x

now

per cases ( b divides x or not b divides x ) ;

case A34: b divides x ; :: thesis: p1 . x = p2 . x

hence p1 . x = p . (x -' b) by A32
.= p2 . x by A33, A34 ;
:: thesis: verum

end;

case A35: not b divides x ; :: thesis: p1 . x = p2 . x

hence p1 . x = 0. L by A32
.= p2 . x by A33, A35 ;
:: thesis: verum

end;

end;

end;

hence p1 . x = p2 . x ; :: thesis: verum

end;

hence p1 = p2 by FUNCT_2:113; :: thesis: verum