let D be non empty set ; :: thesis: for G1, G2 being Element of PFuncs D,REAL holds Sum <*G1,G2*> = G1 + G2
let G1, G2 be Element of PFuncs D,REAL ; :: thesis: Sum <*G1,G2*> = G1 + G2
thus Sum <*G1,G2*> = Sum (<*G1*> ^ <*G2*>) by FINSEQ_1:def 9
.= (Sum <*G1*>) + G2 by Th23
.= G1 + G2 by FINSOP_1:12 ; :: thesis: verum