let D be non empty set ; :: thesis: Sum (<*> (PFuncs D,REAL )) = ([#] D) --> 0
set f = <*> (PFuncs D,REAL );
set o = addpfunc D;
set o0 = ([#] D) --> 0 ;
( addpfunc D is commutative & addpfunc D is associative & the_unity_wrt (addpfunc D) = ([#] D) --> 0 & addpfunc D is having_a_unity ) by Th16, Th17, Th19, Th20;
hence Sum (<*> (PFuncs D,REAL )) = ([#] D) --> 0 by FINSOP_1:11; :: thesis: verum