let S be non void Signature; :: thesis: for X being V6() ManySortedSet of
for Y being ManySortedSet of
for t being Element of (Free S,X) holds S variables_in t c= X
let X be V6() ManySortedSet of ; :: thesis: for Y being ManySortedSet of
for t being Element of (Free S,X) holds S variables_in t c= X
let Y be ManySortedSet of ; :: 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 Th9;
t in Union the Sorts of (Free S,X) ;
then ( t in Union (S -Terms X,(X \/ (the carrier of S --> {0 }))) & dom (S -Terms X,(X \/ (the carrier of S --> {0 }))) = the carrier of S ) by Th25, PARTFUN1:def 4;
then ex s being set st
( s in the carrier of S & t in (S -Terms X,(X \/ (the carrier of S --> {0 }))) . s ) by CARD_5:10;
then variables_in t c= X by Th18;
hence S variables_in t c= X ; :: thesis: verum