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:25;
hence (apply (v,t)) . ((len v) + 1) is type of T by FINSEQ_2:11; :: thesis: verum