theorem :: RELSET_3:12

for X being complex-membered set holds addRel (X,0) = id X