theorem :: AFINSQ_1:98

for x, y being object holds
( dom <%x,y%> = {0,1} & rng <%x,y%> = {x,y} )