let D be non empty set ; :: thesis: Sum (<*> (PFuncs (D,REAL))) = ([#] D) --> 0
set o = addpfunc D;
set o0 = ([#] D) --> 0;
the_unity_wrt (addpfunc D) = ([#] D) --> 0 by Th17;
hence Sum (<*> (PFuncs (D,REAL))) = ([#] D) --> 0 by Th18, FINSOP_1:10; :: thesis: verum