let n be set ; :: thesis: for L being non empty ZeroStr
for b being bag of n holds
( coefficient (Monom ((0. L),b)) = 0. L & term (Monom ((0. L),b)) = EmptyBag n )
let L be non empty ZeroStr ; :: thesis: for b being bag of n holds
( coefficient (Monom ((0. L),b)) = 0. L & term (Monom ((0. L),b)) = EmptyBag n )
let b be bag of n; :: thesis: ( coefficient (Monom ((0. L),b)) = 0. L & term (Monom ((0. L),b)) = EmptyBag n )
set m = (0_ (n,L)) +* (b,(0. L));
reconsider m = (0_ (n,L)) +* (b,(0. L)) as Function of (Bags n), the carrier of L ;
reconsider m = m as Function of (Bags n),L ;
reconsider m = m as Series of n,L ;
A1: b in Bags n by PRE_POLY:def 12;
A2: dom (0_ (n,L)) = dom ((Bags n) --> (0. L)) by POLYNOM1:def 7
.= Bags n by FUNCOP_1:13 ;
then A3: m = (0_ (n,L)) +* (b .--> (0. L)) by A1, FUNCT_7:def 3;
A4: dom (b .--> (0. L)) = {b} by FUNCOP_1:13;
then A5: b in dom (b .--> (0. L)) by TARSKI:def 1;
A6: m . b = ((0_ (n,L)) +* (b .--> (0. L))) . b by A2, A1, FUNCT_7:def 3
.= (b .--> (0. L)) . b by A5, FUNCT_4:13
.= 0. L by FUNCOP_1:72 ;

A7: now

let b9 be bag of n; :: thesis: m . b9 = 0. L

now

per cases ( b9 = b or b9 <> b ) ;

case b9 = b ; :: thesis: m . b9 = 0. L

hence m . b9 = 0. L by A6; :: thesis: verum

end;

case b9 <> b ; :: thesis: m . b9 = 0. L

then not b9 in dom (b .--> (0. L)) by A4, TARSKI:def 1;
hence m . b9 = (0_ (n,L)) . b9 by A3, FUNCT_4:11
.= 0. L by POLYNOM1:22 ;
:: thesis: verum

end;

end;

end;

hence m . b9 = 0. L ; :: thesis: verum

end;

hence coefficient (Monom ((0. L),b)) = 0. L ; :: thesis: term (Monom ((0. L),b)) = EmptyBag n
(Monom ((0. L),b)) . (term (Monom ((0. L),b))) = 0. L by A7;
hence term (Monom ((0. L),b)) = EmptyBag n by Def6; :: thesis: verum