let p1, p2 be Series of n,L; :: thesis: ( ( for b9 being bag of n st b divides b9 holds
( p1 . b9 = p . (b9 -' b) & ( for b9 being bag of n st not b divides b9 holds
p1 . b9 = 0. L ) ) ) & ( for b9 being bag of n st b divides b9 holds
( p2 . b9 = p . (b9 -' b) & ( for b9 being bag of n st not b divides b9 holds
p2 . b9 = 0. L ) ) ) implies p1 = p2 )
assume that
A32: for b9 being bag of n st b divides b9 holds
( p1 . b9 = p . (b9 -' b) & ( for b9 being bag of n st not b divides b9 holds
p1 . b9 = 0. L ) ) and
A33: for b9 being bag of n st b divides b9 holds
( p2 . b9 = p . (b9 -' b) & ( for b9 being bag of n st not b divides b9 holds
p2 . b9 = 0. L ) ) ; :: thesis: p1 = p2
now :: thesis: for x being Element of Bags n holds p1 . x = p2 . x
let x be Element of Bags n; :: thesis: p1 . x = p2 . x
now :: thesis: ( ( b divides x & p1 . x = p2 . x ) or ( not b divides x & p1 . x = p2 . x ) )
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:63; :: thesis: verum