let S be non void Signature; :: thesis: for Y being V8() 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 V8() 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

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 V8() 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