consider p being FinSequence of QC-variables such that
A1: len p = k by FINSEQ_1:24;
take p ; :: thesis: p is k -long
thus len p = k by A1; :: according to FINSEQ_1:def 18 :: thesis: verum