let Al be QC-alphabet ; for k being Nat
for P being QC-pred_symbol of k,Al
for ll being CQC-variable_list of k,Al holds still_not-bound_in (P ! ll) = Bound_Vars (P ! ll)
let k be Nat; for P being QC-pred_symbol of k,Al
for ll being CQC-variable_list of k,Al holds still_not-bound_in (P ! ll) = Bound_Vars (P ! ll)
let P be QC-pred_symbol of k,Al; for ll being CQC-variable_list of k,Al holds still_not-bound_in (P ! ll) = Bound_Vars (P ! ll)
let ll be CQC-variable_list of k,Al; still_not-bound_in (P ! ll) = Bound_Vars (P ! ll)
set l1 = the_arguments_of (P ! ll);
A1:
P ! ll is atomic
by QC_LANG1:def 18;
then consider n being Nat, P9 being QC-pred_symbol of n,Al, ll9 being QC-variable_list of n,Al such that
A2:
the_arguments_of (P ! ll) = ll9
and
A3:
P ! ll = P9 ! ll9
by QC_LANG1:def 23;
Bound_Vars (P ! ll) = Bound_Vars (the_arguments_of (P ! ll))
by A1, SUBSTUT1:3;
then A4:
Bound_Vars (P ! ll) = { ((the_arguments_of (P ! ll)) . i) where i is Nat : ( 1 <= i & i <= len (the_arguments_of (P ! ll)) & (the_arguments_of (P ! ll)) . i in bound_QC-variables Al ) }
by SUBSTUT1:def 7;
still_not-bound_in (P ! ll) = still_not-bound_in ll
by QC_LANG3:5;
then A5:
still_not-bound_in (P ! ll) = variables_in (ll,(bound_QC-variables Al))
by QC_LANG3:2;
A6:
( (<*P9*> ^ ll9) . 1 = P9 & (<*P*> ^ ll) . 1 = P )
by FINSEQ_1:41;
( P ! ll = <*P*> ^ ll & P9 ! ll9 = <*P9*> ^ ll9 )
by QC_LANG1:8;
then
ll9 = ll
by A3, A6, FINSEQ_1:33;
hence
still_not-bound_in (P ! ll) = Bound_Vars (P ! ll)
by A4, A5, A2, QC_LANG3:def 1; verum