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