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 )
assume d in dom F ; :: thesis: Sum (F,{d}) = F . d
hence Sum (F,{d}) = Sum <*(F . d)*> by Th72
.= F . d by FINSOP_1:11 ;
:: thesis: verum