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:11;
A2: (id bound_QC-variables ) * lf = ll by PARTFUN1:37;
thus SepVar (P ! ll) = (ATOMIC P,ll) . (index (P ! ll)),(id bound_QC-variables ) by Def6
.= P ! ll by A2, Def4 ; :: thesis: verum