let I be set ; :: thesis: Sum (<*> (Bags I)) = EmptyBag I
set f = <*> (Bags I);
consider F being Function of NAT,(Bags I) such that
A1: Sum (<*> (Bags I)) = F . (len (<*> (Bags I))) and
A2: F . 0 = EmptyBag I and
for i being Nat
for b being bag of I st i < len (<*> (Bags I)) & b = (<*> (Bags I)) . (i + 1) holds
F . (i + 1) = (F . i) + b by SUM;
thus Sum (<*> (Bags I)) = EmptyBag I by A1, A2; :: thesis: verum