let x be set ; :: thesis: for A being finite 0 -based array holds last (A ^ <%x%>) = x
let A be finite 0 -based array; :: thesis: last (A ^ <%x%>) = x
dom <%x%> = 1 by AFINSQ_1:def 4;
then dom (A ^ <%x%>) = (dom A) +^ 1 by ORDINAL4:def 1
.= succ (dom A) by ORDINAL2:31 ;
then union (dom (A ^ <%x%>)) = len A by ORDINAL2:2;
hence last (A ^ <%x%>) = x by AFINSQ_1:36; :: thesis: verum