let k be Element of NAT ; :: thesis: for P being QC-pred_symbol of k
for ll being CQC-variable_list of k holds the_pred_symbol_of (P ! ll) = P
let P be QC-pred_symbol of k; :: thesis: for ll being CQC-variable_list of k holds the_pred_symbol_of (P ! ll) = P
let ll be CQC-variable_list of k; :: thesis: the_pred_symbol_of (P ! ll) = P
A1: (<*P*> ^ ll) . 1 = P by FINSEQ_1:41;
P ! ll is atomic by QC_LANG1:def 16;
then consider k being Element of NAT , ll9 being QC-variable_list of k, P9 being QC-pred_symbol of k such that
A2: ( the_pred_symbol_of (P ! ll) = P9 & P ! ll = P9 ! ll9 ) by QC_LANG1:def 20;
( P ! ll = <*P*> ^ ll & P9 ! ll9 = <*P9*> ^ ll9 ) by QC_LANG1:6;
hence the_pred_symbol_of (P ! ll) = P by A2, A1, FINSEQ_1:41; :: thesis: verum