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;

now :: thesis: ( ( m . b <> 0. L & ex b₁ being bag of X st
( m . b₁ <> 0. L or ( Support m = {} & b₁ = EmptyBag X ) ) ) or ( m . b = 0. L & ex b₁ being bag of X st
( m . b₁ <> 0. L or ( Support m = {} & b₁ = EmptyBag X ) ) ) )

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

case m . b <> 0. L ; :: thesis: ex b₁ being bag of X st
( m . b₁ <> 0. L or ( Support m = {} & b₁ = EmptyBag X ) )

hence ex b₁ being bag of X st
( m . b₁ <> 0. L or ( Support m = {} & b₁ = EmptyBag X ) ) ; :: thesis: verum

end;

case A2: m . b = 0. L ; :: thesis: ex b₁ being bag of X st
( m . b₁ <> 0. L or ( Support m = {} & b₁ = EmptyBag X ) )

Support m = {}

proof

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;

hence ex b₁ being bag of X st
( m . b₁ <> 0. L or ( Support m = {} & b₁ = EmptyBag X ) ) ; :: thesis: verum

end;

end;

end;

hence ex b₁ being bag of X st
( m . b₁ <> 0. L or ( Support m = {} & b₁ = EmptyBag X ) ) ; :: thesis: verum