let p1, p2 be Series of n,L; :: thesis: ( ( for b' being bag of st b divides b' holds
( p1 . b' = p . (b' -' b) & ( for b' being bag of st not b divides b' holds
p1 . b' = 0. L ) ) ) & ( for b' being bag of st b divides b' holds
( p2 . b' = p . (b' -' b) & ( for b' being bag of st not b divides b' holds
p2 . b' = 0. L ) ) ) implies p1 = p2 )
assume that
A28: for b' being bag of st b divides b' holds
( p1 . b' = p . (b' -' b) & ( for b' being bag of st not b divides b' holds
p1 . b' = 0. L ) ) and
A29: for b' being bag of st b divides b' holds
( p2 . b' = p . (b' -' b) & ( for b' being bag of 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 A30: b divides x ; :: thesis: p1 . x = p2 . x

hence p1 . x = p . (x -' b) by A28
.= p2 . x by A29, A30 ;
:: thesis: verum

end;

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

hence p1 . x = 0. L by A28
.= p2 . x by A29, A31 ;
:: thesis: verum

end;

end;

end;

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

end;

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