let k be Element of NAT ; :: thesis: for ll being CQC-variable_list of k
for P being QC-pred_symbol of k holds SepVar (P ! ll) = P ! ll
let ll be CQC-variable_list of k; :: thesis: for P being QC-pred_symbol of k holds SepVar (P ! ll) = P ! ll
let P be QC-pred_symbol of k; :: thesis: SepVar (P ! ll) = P ! ll
A1: dom ll = dom ll ;
rng ll c= bound_QC-variables by RELAT_1:def 19;
then reconsider lf = ll as PartFunc of NAT,bound_QC-variables by A1, RELSET_1:4;
A2: (id bound_QC-variables) * lf = ll by PARTFUN1:7;
thus SepVar (P ! ll) = (ATOMIC (P,ll)) . ((index (P ! ll)),(id bound_QC-variables)) by Def6
.= P ! ll by A2, Def4 ; :: thesis: verum