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