let b1, b2 be bag of X; :: thesis: ( ( m . b1 <> 0. L or ( Support m = {} & b1 = EmptyBag X ) ) & ( m . b2 <> 0. L or ( Support m = {} & b2 = EmptyBag X ) ) implies b1 = b2 )
assume A3: ( m . b1 <> 0. L or ( Support m = {} & b1 = EmptyBag X ) ) ; :: thesis: ( ( not m . b2 <> 0. L & not ( Support m = {} & b2 = EmptyBag X ) ) or b1 = b2 )
consider b being bag of X such that
A4: for b9 being bag of X st b9 <> b holds
m . b9 = 0. L by Def3;
assume A5: ( m . b2 <> 0. L or ( Support m = {} & b2 = EmptyBag X ) ) ; :: thesis: b1 = b2

now :: thesis: ( ( m . b1 <> 0. L & b1 = b2 ) or ( m . b1 = 0. L & b1 = b2 ) )

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

case A6: m . b1 <> 0. L ; :: thesis: b1 = b2

reconsider b19 = b1 as Element of Bags X by PRE_POLY:def 12;
A7: b19 in Support m by A6, POLYNOM1:def 4;
thus b1 = b by A4, A6
.= b2 by A5, A4, A7 ; :: thesis: verum

end;

case A8: m . b1 = 0. L ; :: thesis: b1 = b2

now :: thesis: ( ( m . b2 <> 0. L & b1 = b2 ) or ( Support m = {} & b2 = EmptyBag X & b1 = b2 ) )

per cases ( m . b2 <> 0. L or ( Support m = {} & b2 = EmptyBag X ) ) by A5;

case A9: m . b2 <> 0. L ; :: thesis: b1 = b2

reconsider b29 = b2 as Element of Bags X by PRE_POLY:def 12;
b29 in Support m by A9, POLYNOM1:def 4;
hence b1 = b2 by A3, A8; :: thesis: verum

end;

case ( Support m = {} & b2 = EmptyBag X ) ; :: thesis: b1 = b2

hence b1 = b2 by A3, A8; :: thesis: verum

end;

end;

end;

hence b1 = b2 ; :: thesis: verum

end;

end;

end;

hence b1 = b2 ; :: thesis: verum