theorem Th11: :: RING_EMB:11

for A being AbGroup
for X being non empty set
for f being Function of A,X
for a, b, c being Element of X st f is bijective holds
addemb (f,a,(addemb (f,b,c))) = addemb (f,(addemb (f,a,b)),c)