let n be set ; :: thesis: for L being non empty ZeroStr
for a being Element of L
for b being bag of n holds coefficient (Monom a,b) = a
let L be non empty ZeroStr ; :: thesis: for a being Element of L
for b being bag of n holds coefficient (Monom a,b) = a
let a be Element of L; :: thesis: for b being bag of n holds coefficient (Monom a,b) = a
let b be bag of n; :: thesis: coefficient (Monom a,b) = a
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;
dom (b .--> a) = {b} by FUNCOP_1:19;
then A2: b in dom (b .--> a) by TARSKI:def 1;
dom (0_ n,L) = dom ((Bags n) --> (0. L)) by POLYNOM1:def 24
.= Bags n by FUNCOP_1:19 ;
then A3: m . b = ((0_ n,L) +* (b .--> a)) . b by A1, FUNCT_7:def 3
.= (b .--> a) . b by A2, FUNCT_4:14
.= a by FUNCOP_1:87 ;

per cases ( m . b <> 0. L or m . b = 0. L ) ;

suppose m . b <> 0. L ; :: thesis: coefficient (Monom a,b) = a

hence coefficient (Monom a,b) = a by A3, Def6; :: thesis: verum

end;

suppose m . b = 0. L ; :: thesis: coefficient (Monom a,b) = a

hence coefficient (Monom a,b) = a by A3, Th8; :: thesis: verum

end;

end;