theorem Th23: :: ARYTM_0:23

for x, y, z being Element of REAL holds + (x,(+ (y,z))) = + ((+ (x,y)),z)