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

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