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 ;

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 ;

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 ;

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

hence
(0_ (X,L)) +* (b,a) is Monomial of X,L
; :: thesis: verumper cases
( a <> 0. L or a = 0. L )
;

end;

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}

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;u in {b}

proof

b in Support m
by A2, A5, A6, POLYNOM1:def 4;
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;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

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

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

end;

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

hence
(0_ (X,L)) +* (b,a) is Monomial of X,L
by Th6; :: thesis: verumassume
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;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