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