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