let k be Element of NAT ; :: thesis: for p being QC-pred_symbol of k
for ll being QC-variable_list of k holds <*p*> ^ ll is FinSequence of [:NAT ,NAT :]
let p be QC-pred_symbol of k; :: thesis: for ll being QC-variable_list of k holds <*p*> ^ ll is FinSequence of [:NAT ,NAT :]
let ll be QC-variable_list of k; :: thesis: <*p*> ^ ll is FinSequence of [:NAT ,NAT :]
QC-variables c= [:NAT ,NAT :] by Th2;
then A1: rng ll c= [:NAT ,NAT :] by XBOOLE_1:1;
k -ary_QC-pred_symbols c= [:NAT ,NAT :] by Th10, XBOOLE_1:1;
then rng <*p*> c= [:NAT ,NAT :] by 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:44;
hence <*p*> ^ ll is FinSequence of [:NAT ,NAT :] by FINSEQ_1:def 4; :: thesis: verum