let X be set ; :: thesis: for L being non empty ZeroStr
for a being Element of L holds
( term (a | (X,L)) = EmptyBag X & coefficient (a | (X,L)) = a )
let L be non empty ZeroStr ; :: thesis: for a being Element of L holds
( term (a | (X,L)) = EmptyBag X & coefficient (a | (X,L)) = a )
let a be Element of L; :: thesis: ( term (a | (X,L)) = EmptyBag X & coefficient (a | (X,L)) = a )
set m = (0_ (X,L)) +* ((EmptyBag X),a);
reconsider m = (0_ (X,L)) +* ((EmptyBag X),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 ;
A1: EmptyBag X in dom ((EmptyBag X) .--> a) by TARSKI:def 1;
dom (0_ (X,L)) = dom ((Bags X) --> (0. L)) by POLYNOM1:def 8
.= Bags X ;
then m . (EmptyBag X) = ((0_ (X,L)) +* ((EmptyBag X) .--> a)) . (EmptyBag X) by FUNCT_7:def 3
.= ((EmptyBag X) .--> a) . (EmptyBag X) by A1, FUNCT_4:13
.= a by FUNCOP_1:72 ;
hence ( term (a | (X,L)) = EmptyBag X & coefficient (a | (X,L)) = a ) by Lm2; :: thesis: verum