let S be non void Signature; :: thesis: for Y being V5() ManySortedSet of
for t being Term of S,Y
for p being Element of dom t holds variables_in (t | p) c= variables_in t
let Y be V5() ManySortedSet of ; :: thesis: for t being Term of S,Y
for p being Element of dom t holds variables_in (t | p) c= variables_in t
let t be Term of S,Y; :: thesis: for p being Element of dom t holds variables_in (t | p) c= variables_in t
let p be Element of dom t; :: thesis: variables_in (t | p) c= variables_in t
reconsider q = t | p as Term of S,Y ;
A1: rng (t | p) c= rng t by TREES_2:34;
let s be set ; :: according to PBOOLE:def 5 :: thesis: ( not s in the carrier of S or (variables_in (t | p)) . s c= (variables_in t) . s )
assume A2: s in the carrier of S ; :: thesis: (variables_in (t | p)) . s c= (variables_in t) . s
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (variables_in (t | p)) . s or x in (variables_in t) . s )
assume x in (variables_in (t | p)) . s ; :: thesis: x in (variables_in t) . s
then x in { (a `1 ) where a is Element of rng q : a `2 = s } by A2, Def3;
then consider a being Element of rng (t | p) such that
A3: ( x = a `1 & a `2 = s ) ;
a in rng (t | p) ;
then x in { (b `1 ) where b is Element of rng t : b `2 = s } by A1, A3;
hence x in (variables_in t) . s by A2, Def3; :: thesis: verum