let S be non void Signature; :: thesis: for Y being non-empty ManySortedSet of the carrier of S
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 non-empty ManySortedSet of the carrier of S; :: 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 ;
let s be object ; :: according to PBOOLE:def 2 :: thesis: ( not s in the carrier of S or (variables_in (t | p)) . s c= (variables_in t) . s )
assume A1: s in the carrier of S ; :: thesis: (variables_in (t | p)) . s c= (variables_in t) . s
let x be object ; :: 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 A1, Def2;
then consider a being Element of rng (t | p) such that
A2: ( x = a `1 & a `2 = s ) ;
( rng (t | p) c= rng t & a in rng (t | p) ) by TREES_2:32;
then x in { (b `1) where b is Element of rng t : b `2 = s } by A2;
hence x in (variables_in t) . s by A1, Def2; :: thesis: verum