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 b1 being bag of X st
( m . b1 <> 0. L or ( Support m = {} & b1 = EmptyBag X ) ) ) or ( m . b = 0. L & ex b1 being bag of X st
( m . b1 <> 0. L or ( Support m = {} & b1 = EmptyBag X ) ) ) )
per cases ( m . b <> 0. L or m . b = 0. L ) ;
case m . b <> 0. L ; :: thesis: ex b1 being bag of X st
( m . b1 <> 0. L or ( Support m = {} & b1 = EmptyBag X ) )
hence ex b1 being bag of X st
( m . b1 <> 0. L or ( Support m = {} & b1 = EmptyBag X ) ) ; :: thesis: verum
end;
case A2: m . b = 0. L ; :: thesis: ex b1 being bag of X st
( m . b1 <> 0. L or ( Support m = {} & b1 = 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 b1 being bag of X st
( m . b1 <> 0. L or ( Support m = {} & b1 = EmptyBag X ) ) ; :: thesis: verum
end;
end;
end;
hence ex b1 being bag of X st
( m . b1 <> 0. L or ( Support m = {} & b1 = EmptyBag X ) ) ; :: thesis: verum