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