theorem Th1: :: AMI_8:1

for x1, x2, x3, x4 being object holds dom <%x1,x2,x3,x4%> = {0,1,2,3}