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