let A be QC-alphabet ; 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; 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; 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; 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; verum