let A be QC-alphabet ; :: thesis: for k being Nat
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):]
let k be Nat; :: thesis: for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):]
let p be QC-pred_symbol of k,A; :: thesis: for ll being QC-variable_list of k,A
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):]
let ll be QC-variable_list of k,A; :: thesis: for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):]
QC-pred_symbols A c= [:NAT,(QC-symbols A):] by QC_LANG1:6;
then k -ary_QC-pred_symbols A c= [:NAT,(QC-symbols A):] ;
then A1: rng <*p*> c= [:NAT,(QC-symbols A):] ;
QC-variables A c= [:NAT,(QC-symbols A):] by QC_LANG1:4;
then rng ll c= [:NAT,(QC-symbols A):] ;
then (rng <*p*>) \/ (rng ll) c= [:NAT,(QC-symbols A):] by A1, XBOOLE_1:8;
then rng (<*p*> ^ ll) c= [:NAT,(QC-symbols A):] by FINSEQ_1:31;
then <*p*> ^ ll is FinSequence of [:NAT,(QC-symbols A):] by FINSEQ_1:def 4;
then <*p*> ^ ll in [:NAT,(QC-symbols A):] * by FINSEQ_1:def 11;
hence for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):] by ZFMISC_1:def 2; :: thesis: verum