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

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