let D be non empty set ; :: thesis: for F being PartFunc of D,REAL
for d being Element of D st d in dom F holds
Sum (F,{d}) = F . d
let F be PartFunc of D,REAL; :: thesis: for d being Element of D st d in dom F holds
Sum (F,{d}) = F . d
let d be Element of D; :: thesis: ( d in dom F implies Sum (F,{d}) = F . d )
reconsider Fd = F . d as Element of REAL by XREAL_0:def 1;
assume d in dom F ; :: thesis: Sum (F,{d}) = F . d
hence Sum (F,{d}) = Sum <*Fd*> by Th69
.= F . d by FINSOP_1:11 ;
:: thesis: verum