let X be set ; :: thesis: for L being non empty ZeroStr
for b being bag of X holds Monom ((0. L),b) = 0_ (X,L)
let L be non empty ZeroStr ; :: thesis: for b being bag of X holds Monom ((0. L),b) = 0_ (X,L)
let b be bag of X; :: thesis: Monom ((0. L),b) = 0_ (X,L)
A1: dom (0_ (X,L)) = Bags X by FUNCT_2:def 1;
for x being object st x in Bags X holds
(Monom ((0. L),b)) . x = (0_ (X,L)) . x

proof

let x be object ; :: thesis: ( x in Bags X implies (Monom ((0. L),b)) . x = (0_ (X,L)) . x )
assume A2: x in Bags X ; :: thesis: (Monom ((0. L),b)) . x = (0_ (X,L)) . x

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

suppose x = b ; :: thesis: (Monom ((0. L),b)) . x = (0_ (X,L)) . x

hence (Monom ((0. L),b)) . x = 0. L by A1, A2, FUNCT_7:31
.= (0_ (X,L)) . x by A2, POLYNOM1:22 ;
:: thesis: verum

end;

suppose x <> b ; :: thesis: (Monom ((0. L),b)) . x = (0_ (X,L)) . x

hence (Monom ((0. L),b)) . x = (0_ (X,L)) . x by FUNCT_7:32; :: thesis: verum

end;

end;

end;

hence Monom ((0. L),b) = 0_ (X,L) ; :: thesis: verum