consider b being bag of X such that

A1: for b9 being bag of X st b9 <> b holds

m . b9 = 0. L by Def3;

_{1} being bag of X st

( m . b_{1} <> 0. L or ( Support m = {} & b_{1} = EmptyBag X ) )
; :: thesis: verum

A1: for b9 being bag of X st b9 <> b holds

m . b9 = 0. L by Def3;

now :: thesis: ( ( m . b <> 0. L & ex b_{1} being bag of X st

( m . b_{1} <> 0. L or ( Support m = {} & b_{1} = EmptyBag X ) ) ) or ( m . b = 0. L & ex b_{1} being bag of X st

( m . b_{1} <> 0. L or ( Support m = {} & b_{1} = EmptyBag X ) ) ) )end;

hence
ex b( m . b

( m . b

per cases
( m . b <> 0. L or m . b = 0. L )
;

end;

case
m . b <> 0. L
; :: thesis: ex b_{1} being bag of X st

( m . b_{1} <> 0. L or ( Support m = {} & b_{1} = EmptyBag X ) )

( m . b

hence
ex b_{1} being bag of X st

( m . b_{1} <> 0. L or ( Support m = {} & b_{1} = EmptyBag X ) )
; :: thesis: verum

end;( m . b

case A2:
m . b = 0. L
; :: thesis: ex b_{1} being bag of X st

( m . b_{1} <> 0. L or ( Support m = {} & b_{1} = EmptyBag X ) )

( m . b

Support m = {}
_{1} being bag of X st

( m . b_{1} <> 0. L or ( Support m = {} & b_{1} = EmptyBag X ) )
; :: thesis: verum

end;proof

hence
ex b
assume
Support m <> {}
; :: thesis: contradiction

then reconsider sm = Support m as non empty Subset of (Bags X) ;

set c = the Element of sm;

m . the Element of sm <> 0. L by POLYNOM1:def 4;

hence contradiction by A1, A2; :: thesis: verum

end;then reconsider sm = Support m as non empty Subset of (Bags X) ;

set c = the Element of sm;

m . the Element of sm <> 0. L by POLYNOM1:def 4;

hence contradiction by A1, A2; :: thesis: verum

( m . b

( m . b