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