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