dom (b .--> a) = {b} by FUNCOP_1:13;
then A1: b in dom (b .--> a) by TARSKI:def 1;
set m = (0_ (X,L)) +* (b,a);
reconsider m = (0_ (X,L)) +* (b,a) as Function of (Bags X), the carrier of L ;
reconsider m = m as Function of (Bags X),L ;
reconsider m = m as Series of X,L ;
A2: b in Bags X by PRE_POLY:def 12;
A3: dom (0_ (X,L)) = dom ((Bags X) --> (0. L)) by POLYNOM1:def 8
.= Bags X by FUNCOP_1:13 ;
then A4: m = (0_ (X,L)) +* (b .--> a) by A2, FUNCT_7:def 3;
A5: m . b = ((0_ (X,L)) +* (b .--> a)) . b by A3, A2, FUNCT_7:def 3
.= (b .--> a) . b by A1, FUNCT_4:13
.= a by FUNCOP_1:72 ;

now :: thesis: ( ( a <> 0. L & (0_ (X,L)) +* (b,a) is Monomial of X,L ) or ( a = 0. L & (0_ (X,L)) +* (b,a) is Monomial of X,L ) )

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

case A6: a <> 0. L ; :: thesis: (0_ (X,L)) +* (b,a) is Monomial of X,L

A7: for u being object st u in Support m holds
u in {b}

proof

let u be object ; :: thesis: ( u in Support m implies u in {b} )
assume A8: u in Support m ; :: thesis: u in {b}
assume not u in {b} ; :: thesis: contradiction
then A9: not u in dom (b .--> a) ;
reconsider u = u as bag of X by A8;
m . u = (0_ (X,L)) . u by A4, A9, FUNCT_4:11
.= 0. L by POLYNOM1:22 ;
hence contradiction by A8, POLYNOM1:def 4; :: thesis: verum

end;

b in Support m by A2, A5, A6, POLYNOM1:def 4;
then for u being object st u in {b} holds
u in Support m by TARSKI:def 1;
then Support m = {b} by A7, TARSKI:2;
hence (0_ (X,L)) +* (b,a) is Monomial of X,L by Th6; :: thesis: verum

end;

case A10: a = 0. L ; :: thesis: (0_ (X,L)) +* (b,a) is Monomial of X,L

now :: thesis: not Support m <> {}

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;
then not the Element of sm in {b} by A5, A10, TARSKI:def 1;
then A11: not the Element of sm in dom (b .--> a) ;
reconsider c = the Element of sm as bag of X ;
m . c = (0_ (X,L)) . c by A4, A11, FUNCT_4:11
.= 0. L by POLYNOM1:22 ;
hence contradiction by POLYNOM1:def 4; :: thesis: verum

end;

hence (0_ (X,L)) +* (b,a) is Monomial of X,L by Th6; :: thesis: verum

end;

end;

end;

hence (0_ (X,L)) +* (b,a) is Monomial of X,L ; :: thesis: verum