dom (b .--> a) = {b} by FUNCOP_1:19;
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 24
.= Bags X by FUNCOP_1:19 ;
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:14
.= a by FUNCOP_1:87 ;

now

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 set st u in Support m holds
u in {b}

proof

let u be set ; :: 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) by FUNCOP_1:19;
reconsider u = u as bag of X by A8;
m . u = (0_ X,L) . u by A4, A9, FUNCT_4:12
.= 0. L by POLYNOM1:81 ;
hence contradiction by A8, POLYNOM1:def 9; :: thesis: verum

end;

b in Support m by A2, A5, A6, POLYNOM1:def 9;
then for u being set 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

assume Support m <> {} ; :: thesis: contradiction
then reconsider sm = Support m as non empty Subset of (Bags X) ;
consider c being Element of sm;
m . c <> 0. L by POLYNOM1:def 9;
then not c in {b} by A5, A10, TARSKI:def 1;
then A12: not c in dom (b .--> a) by FUNCOP_1:19;
reconsider c = c as bag of X ;
m . c = (0_ X,L) . c by A4, A12, FUNCT_4:12
.= 0. L by POLYNOM1:81 ;
hence contradiction by POLYNOM1:def 9; :: 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