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:60
.= (Sum <*G1,G2*>) + G3 by Th23
.= (G1 + G2) + G3 by Th26 ; :: thesis: verum