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

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