let A be QC-alphabet ; :: thesis: for p being Element of QC-WFF A
for V being non empty Subset of (QC-variables A) 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 Nat : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in V ) } )
let p be Element of QC-WFF A; :: thesis: for V being non empty Subset of (QC-variables A) 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 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 A); :: 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 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 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 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 Nat : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in V ) } ; :: thesis: verum