let k be Element of NAT ; :: thesis: for P being QC-pred_symbol of k
for ll being CQC-variable_list of holds still_not-bound_in (P ! ll) c= Bound_Vars (P ! ll)
let P be QC-pred_symbol of k; :: thesis: for ll being CQC-variable_list of holds still_not-bound_in (P ! ll) c= Bound_Vars (P ! ll)
let ll be CQC-variable_list of ; :: thesis: still_not-bound_in (P ! ll) c= Bound_Vars (P ! ll)
set l1 = the_arguments_of (P ! ll);
A1: P ! ll is atomic by QC_LANG1:def 17;
then Bound_Vars (P ! ll) = Bound_Vars (the_arguments_of (P ! ll)) by SUBSTUT1:3;
then A2: Bound_Vars (P ! ll) = { ((the_arguments_of (P ! ll)) . i) where i is Element of NAT : ( 1 <= i & i <= len (the_arguments_of (P ! ll)) & (the_arguments_of (P ! ll)) . i in bound_QC-variables ) } by SUBSTUT1:def 7;
still_not-bound_in (P ! ll) = still_not-bound_in ll by QC_LANG3:9;
then A3: still_not-bound_in (P ! ll) = variables_in ll,bound_QC-variables by QC_LANG3:6;
consider n being Element of NAT , P' being QC-pred_symbol of n, ll' being QC-variable_list of such that
A4: ( the_arguments_of (P ! ll) = ll' & P ! ll = P' ! ll' ) by A1, QC_LANG1:def 22;
A5: ( P ! ll = <*P*> ^ ll & P' ! ll' = <*P'*> ^ ll' ) by QC_LANG1:23;
( (<*P'*> ^ ll') . 1 = P' & (<*P*> ^ ll) . 1 = P ) by FINSEQ_1:58;
then ll' = ll by A4, A5, FINSEQ_1:46;
hence still_not-bound_in (P ! ll) c= Bound_Vars (P ! ll) by A2, A3, A4, QC_LANG3:def 2; :: thesis: verum