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 Th20
.= G1 + G2 by FINSOP_1:11 ; :: thesis: verum