let D be non empty set ; :: thesis: for m1, m2 being Multiset of D
for a being Element of D holds (m1 [*] m2) . a = (m1 . a) + (m2 . a)
reconsider N = <NAT,+,0> as non empty multMagma ;
let m1, m2 be Multiset of D; :: thesis: for a being Element of D holds (m1 [*] m2) . a = (m1 . a) + (m2 . a)
let a be Element of D; :: thesis: (m1 [*] m2) . a = (m1 . a) + (m2 . a)
reconsider f1 = m1, f2 = m2 as Element of (.: (N,D)) ;
thus (m1 [*] m2) . a = (f1 . a) * (f2 . a) by Th21
.= (m1 . a) + (m2 . a) by MONOID_0:45 ; :: thesis: verum