let b1, b2 be bag of ; :: 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 )
assume A4: ( m . b2 <> 0. L or ( Support m = {} & b2 = EmptyBag X ) ) ; :: thesis: b1 = b2
consider b being bag of such that
A5: for b' being bag of st b' <> b holds
m . b' = 0. L by Def4;

now

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

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

reconsider b1' = b1 as Element of Bags X by POLYNOM1:def 14;
A7: b1' in Support m by A6, POLYNOM1:def 9;
thus b1 = b by A5, A6
.= b2 by A4, A5, A7 ; :: thesis: verum

end;

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

now

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

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

reconsider b2' = b2 as Element of Bags X by POLYNOM1:def 14;
b2' in Support m by A9, POLYNOM1:def 9;
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