A1: ( dom (B "**" F) = dom F & dom F = Seg (len F) ) by FUNCT_2:def 1, FINSEQ_1:def 3;
then reconsider BF = B "**" F as FinSequence by FINSEQ_1:def 2;
len BF = len F by A1, FINSEQ_1:def 3;
hence ( B "**" F is len F -element & B "**" F is FinSequence-like ) by CARD_1:def 7; :: thesis: verum