let A be QC-alphabet ; :: thesis: for k being Nat
for h being FinSequence holds
( h is CQC-variable_list of k,A iff ( h is FinSequence of bound_QC-variables A & len h = k ) )
let k be Nat; :: thesis: for h being FinSequence holds
( h is CQC-variable_list of k,A iff ( h is FinSequence of bound_QC-variables A & len h = k ) )
let h be FinSequence; :: thesis: ( h is CQC-variable_list of k,A iff ( h is FinSequence of bound_QC-variables A & len h = k ) )
thus ( h is CQC-variable_list of k,A implies ( h is FinSequence of bound_QC-variables A & len h = k ) ) :: thesis: ( h is FinSequence of bound_QC-variables A & len h = k implies h is CQC-variable_list of k,A )
proof
assume A1: h is CQC-variable_list of k,A ; :: thesis: ( h is FinSequence of bound_QC-variables A & len h = k )
then rng h c= bound_QC-variables A by RELAT_1:def 19;
hence h is FinSequence of bound_QC-variables A by FINSEQ_1:def 4; :: thesis: len h = k
thus len h = k by A1, CARD_1:def 7; :: thesis: verum
end;
thus ( h is FinSequence of bound_QC-variables A & len h = k implies h is CQC-variable_list of k,A ) :: thesis: verum
proof
assume that
A2: h is FinSequence of bound_QC-variables A and
A3: len h = k ; :: thesis: h is CQC-variable_list of k,A
rng h c= bound_QC-variables A by A2, FINSEQ_1:def 4;
then rng h c= QC-variables A by XBOOLE_1:1;
hence h is CQC-variable_list of k,A by A2, A3, CARD_1:def 7, FINSEQ_1:def 4; :: thesis: verum
end;