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