consider p being FinSequence of QC-variables A such that
A1: len p = k by FINSEQ_1:19;
take p ; :: thesis: p is k -element
thus len p = k by A1; :: according to CARD_1:def 7 :: thesis: verum