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

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 ) )end;

hence
b1 = b2
; :: thesis: verumper cases
( m . b1 <> 0. L or m . b1 = 0. L )
;

end;

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;A7: b19 in Support m by A6, POLYNOM1:def 4;

thus b1 = b by A4, A6

.= b2 by A5, A4, A7 ; :: thesis: verum

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

end;

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

hence
b1 = b2
; :: thesis: verumend;