theorem Th11: :: LPSPACE1:11

for A being non empty set
for f, g, h being Element of PFuncs (A,REAL) holds (addpfunc A) . (f,((addpfunc A) . (g,h))) = (addpfunc A) . (((addpfunc A) . (f,g)),h) by RFUNCT_3:15, BINOP_1:def 3;