let k be Nat; :: thesis: for A being QC-alphabet
for P being QC-pred_symbol of k,A
for l being QC-variable_list of k,A holds still_not-bound_in (P ! l) = still_not-bound_in l
let A be QC-alphabet ; :: thesis: for P being QC-pred_symbol of k,A
for l being QC-variable_list of k,A holds still_not-bound_in (P ! l) = still_not-bound_in l
let P be QC-pred_symbol of k,A; :: thesis: for l being QC-variable_list of k,A holds still_not-bound_in (P ! l) = still_not-bound_in l
let l be QC-variable_list of k,A; :: thesis: still_not-bound_in (P ! l) = still_not-bound_in l
A1: P ! l is atomic ;
then the_arguments_of (P ! l) = l by QC_LANG1:def 23;
hence still_not-bound_in (P ! l) = still_not-bound_in l by A1, Th4; :: thesis: verum