let k be Element of NAT ; :: thesis: for P being QC-pred_symbol of
for ll being CQC-variable_list of k holds the_pred_symbol_of (P ! ll) = P
let P be QC-pred_symbol of ; :: 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:58;
P ! ll is atomic by QC_LANG1:def 17;
then consider k being Element of NAT , ll' being QC-variable_list of k, P' being QC-pred_symbol of such that
A2: ( the_pred_symbol_of (P ! ll) = P' & P ! ll = P' ! ll' ) by QC_LANG1:def 21;
( P ! ll = <*P*> ^ ll & P' ! ll' = <*P'*> ^ ll' ) by QC_LANG1:23;
hence the_pred_symbol_of (P ! ll) = P by A2, A1, FINSEQ_1:58; :: thesis: verum