let n be set ; :: thesis: for L being non trivial ZeroStr

for a being non zero Element of L

for b being bag of n holds term (Monom (a,b)) = b

let L be non trivial ZeroStr ; :: thesis: for a being non zero Element of L

for b being bag of n holds term (Monom (a,b)) = b

let a be non zero Element of L; :: thesis: for b being bag of n holds term (Monom (a,b)) = b

let b be bag of n; :: thesis: term (Monom (a,b)) = b

set m = (0_ (n,L)) +* (b,a);

reconsider m = (0_ (n,L)) +* (b,a) 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: b in dom (b .--> a) by TARSKI:def 1;

dom (0_ (n,L)) = dom ((Bags n) --> (0. L)) by POLYNOM1:def 8

.= Bags n ;

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

.= (b .--> a) . b by A2, FUNCT_4:13

.= a by FUNCOP_1:72 ;

then m . b <> 0. L ;

hence term (Monom (a,b)) = b by Def5; :: thesis: verum

for a being non zero Element of L

for b being bag of n holds term (Monom (a,b)) = b

let L be non trivial ZeroStr ; :: thesis: for a being non zero Element of L

for b being bag of n holds term (Monom (a,b)) = b

let a be non zero Element of L; :: thesis: for b being bag of n holds term (Monom (a,b)) = b

let b be bag of n; :: thesis: term (Monom (a,b)) = b

set m = (0_ (n,L)) +* (b,a);

reconsider m = (0_ (n,L)) +* (b,a) 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: b in dom (b .--> a) by TARSKI:def 1;

dom (0_ (n,L)) = dom ((Bags n) --> (0. L)) by POLYNOM1:def 8

.= Bags n ;

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

.= (b .--> a) . b by A2, FUNCT_4:13

.= a by FUNCOP_1:72 ;

then m . b <> 0. L ;

hence term (Monom (a,b)) = b by Def5; :: thesis: verum