let x1, x2, x3, x4 be object ; :: thesis: dom <%x1,x2,x3,x4%> = {0,1,2,3}
A1: len <%x1,x2,x3%> = 3 by AFINSQ_1:39;
thus dom <%x1,x2,x3,x4%> = (len <%x1,x2,x3%>) + (len <%x4%>) by AFINSQ_1:def 3
.= 3 + 1 by A1, AFINSQ_1:34
.= {0,1,2,3} by CARD_1:52 ; :: thesis: verum