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 8

.= Bags n ;

then A3: m = (0_ (n,L)) +* (b .--> (0. L)) by A1, FUNCT_7:def 3;

A4: b in dom (b .--> (0. L)) by TARSKI:def 1;

A5: m . b = ((0_ (n,L)) +* (b .--> (0. L))) . b by A2, A1, FUNCT_7:def 3

.= (b .--> (0. L)) . b by A4, FUNCT_4:13

.= 0. L by FUNCOP_1:72 ;

(Monom ((0. L),b)) . (term (Monom ((0. L),b))) = 0. L by A6;

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

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 8

.= Bags n ;

then A3: m = (0_ (n,L)) +* (b .--> (0. L)) by A1, FUNCT_7:def 3;

A4: b in dom (b .--> (0. L)) by TARSKI:def 1;

A5: m . b = ((0_ (n,L)) +* (b .--> (0. L))) . b by A2, A1, FUNCT_7:def 3

.= (b .--> (0. L)) . b by A4, FUNCT_4:13

.= 0. L by FUNCOP_1:72 ;

A6: now :: thesis: for b9 being bag of n holds m . b9 = 0. L

hence
coefficient (Monom ((0. L),b)) = 0. L
; :: thesis: term (Monom ((0. L),b)) = EmptyBag nlet b9 be bag of n; :: thesis: m . b9 = 0. L

end;now :: thesis: ( ( b9 = b & m . b9 = 0. L ) or ( b9 <> b & m . b9 = 0. L ) )end;

hence
m . b9 = 0. L
; :: thesis: verumper cases
( b9 = b or b9 <> b )
;

end;

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

then
not b9 in dom (b .--> (0. L))
by TARSKI:def 1;

hence m . b9 = (0_ (n,L)) . b9 by A3, FUNCT_4:11

.= 0. L by POLYNOM1:22 ;

:: thesis: verum

end;hence m . b9 = (0_ (n,L)) . b9 by A3, FUNCT_4:11

.= 0. L by POLYNOM1:22 ;

:: thesis: verum

(Monom ((0. L),b)) . (term (Monom ((0. L),b))) = 0. L by A6;

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