let S be non void Signature; :: thesis: for X being V9() ManySortedSet of the carrier of S

for Y being ManySortedSet of the carrier of S

for t being Element of (Free (S,X)) holds S variables_in t c= X

let X be V9() ManySortedSet of the carrier of S; :: thesis: for Y being ManySortedSet of the carrier of S

for t being Element of (Free (S,X)) holds S variables_in t c= X

let Y be ManySortedSet of the carrier of S; :: thesis: for t being Element of (Free (S,X)) holds S variables_in t c= X

let t be Element of (Free (S,X)); :: thesis: S variables_in t c= X

set Z = X (\/) ( the carrier of S --> {0});

reconsider t = t as Term of S,(X (\/) ( the carrier of S --> {0})) by Th8;

t in Union the Sorts of (Free (S,X)) ;

then A1: t in Union (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) by Th24;

dom (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) = the carrier of S by PARTFUN1:def 2;

then ex s being object st

( s in the carrier of S & t in (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s ) by A1, CARD_5:2;

then variables_in t c= X by Th17;

hence S variables_in t c= X ; :: thesis: verum

for Y being ManySortedSet of the carrier of S

for t being Element of (Free (S,X)) holds S variables_in t c= X

let X be V9() ManySortedSet of the carrier of S; :: thesis: for Y being ManySortedSet of the carrier of S

for t being Element of (Free (S,X)) holds S variables_in t c= X

let Y be ManySortedSet of the carrier of S; :: thesis: for t being Element of (Free (S,X)) holds S variables_in t c= X

let t be Element of (Free (S,X)); :: thesis: S variables_in t c= X

set Z = X (\/) ( the carrier of S --> {0});

reconsider t = t as Term of S,(X (\/) ( the carrier of S --> {0})) by Th8;

t in Union the Sorts of (Free (S,X)) ;

then A1: t in Union (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) by Th24;

dom (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) = the carrier of S by PARTFUN1:def 2;

then ex s being object st

( s in the carrier of S & t in (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s ) by A1, CARD_5:2;

then variables_in t c= X by Th17;

hence S variables_in t c= X ; :: thesis: verum