let Al be QC-alphabet ; :: thesis: for k being Nat
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds the_arity_of P = len l
let k be Nat; :: thesis: for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds the_arity_of P = len l
let l be CQC-variable_list of k,Al; :: thesis: for P being QC-pred_symbol of k,Al holds the_arity_of P = len l
let P be QC-pred_symbol of k,Al; :: thesis: the_arity_of P = len l
thus len l = k by CARD_1:def 7
.= the_arity_of P by QC_LANG1:11 ; :: thesis: verum