let x1, x2, x3, x4, x5, x6 be object ; :: thesis: dom <%x1,x2,x3,x4,x5,x6%> = {0,1,2,3,4,5}
A1: len <%x1,x2,x3,x4,x5%> = 5 by Th4, CARD_1:53;
thus dom <%x1,x2,x3,x4,x5,x6%> = (len <%x1,x2,x3,x4,x5%>) + (len <%x6%>) by AFINSQ_1:def 3
.= 5 + 1 by A1, AFINSQ_1:34
.= {0,1,2,3,4,5} by CARD_1:54 ; :: thesis: verum