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 ;
the_unity_wrt (addpfunc D) = ([#] D) --> 0 by Th19;
hence Sum (<*> (PFuncs D,REAL )) = ([#] D) --> 0 by Th20, FINSOP_1:11; :: thesis: verum