let k be Element of NAT ; :: thesis: for V being non empty Subset of QC-variables
for P being QC-pred_symbol of k
for l being QC-variable_list of holds
( Vars (P ! l),V = variables_in l,V & Vars (P ! l),V = { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in V ) } )
let V be non empty Subset of QC-variables ; :: thesis: for P being QC-pred_symbol of k
for l being QC-variable_list of holds
( Vars (P ! l),V = variables_in l,V & Vars (P ! l),V = { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in V ) } )
let P be QC-pred_symbol of k; :: thesis: for l being QC-variable_list of holds
( Vars (P ! l),V = variables_in l,V & Vars (P ! l),V = { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in V ) } )
let l be QC-variable_list of ; :: thesis: ( Vars (P ! l),V = variables_in l,V & Vars (P ! l),V = { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in V ) } )
A1: P ! l is atomic by QC_LANG1:def 17;
then the_arguments_of (P ! l) = l by QC_LANG1:def 22;
hence ( Vars (P ! l),V = variables_in l,V & Vars (P ! l),V = { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in V ) } ) by A1, Th47; :: thesis: verum