let p be Element of QC-WFF ; :: thesis: for V being non empty Subset of QC-variables st p is atomic holds
( Vars (p,V) = variables_in ((the_arguments_of p),V) & Vars (p,V) = { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in V ) } )
let V be non empty Subset of QC-variables; :: thesis: ( p is atomic implies ( Vars (p,V) = variables_in ((the_arguments_of p),V) & Vars (p,V) = { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in V ) } ) )
assume p is atomic ; :: thesis: ( Vars (p,V) = variables_in ((the_arguments_of p),V) & Vars (p,V) = { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in V ) } )
hence Vars (p,V) = variables_in ((the_arguments_of p),V) by Lm2; :: thesis: Vars (p,V) = { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in V ) }
hence Vars (p,V) = { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in V ) } ; :: thesis: verum