let k be Element of NAT ; :: thesis: for ll being CQC-variable_list of
for P being QC-pred_symbol of k holds SepVar (P ! ll) = P ! ll
let ll be CQC-variable_list of ; :: 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
( rng ll c= bound_QC-variables & dom ll = dom ll ) by RELAT_1:def 19;
then reconsider lf = ll as PartFunc of NAT ,bound_QC-variables by RELSET_1:11;
A1: (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 A1, Def4 ; :: thesis: verum