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 holds <*p*> ^ ll is FinSequence of [:NAT,(QC-symbols A):]
let k be Nat; :: thesis: for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds <*p*> ^ ll is FinSequence of [:NAT,(QC-symbols A):]
let p be QC-pred_symbol of k,A; :: thesis: for ll being QC-variable_list of k,A holds <*p*> ^ ll is FinSequence of [:NAT,(QC-symbols A):]
let ll be QC-variable_list of k,A; :: thesis: <*p*> ^ ll is FinSequence of [:NAT,(QC-symbols A):]
QC-variables A c= [:NAT,(QC-symbols A):] by Th4;
then A1: rng ll c= [:NAT,(QC-symbols A):] ;
QC-pred_symbols A c= [:NAT,(QC-symbols A):] by Th6;
then k -ary_QC-pred_symbols A c= [:NAT,(QC-symbols A):] ;
then rng <*p*> 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;
hence <*p*> ^ ll is FinSequence of [:NAT,(QC-symbols A):] by FINSEQ_1:def 4; :: thesis: verum