A1: (len v) + 1 >= 1 by NAT_1:11;
len (apply v,t) = (len v) + 1 by Def19;
then (len v) + 1 in dom (apply v,t) by A1, FINSEQ_3:27;
hence (apply v,t) . ((len v) + 1) is type of T by FINSEQ_2:13; :: thesis: verum