:: deftheorem Def5 defines [* ARYTM_0:def 5 :
for x, y being Element of REAL holds
( ( y = 0 implies [*x,y*] = x ) & ( not y = 0 implies [*x,y*] = (0,1) --> (x,y) ) );