let S be non void Signature; :: thesis: for X being V6() ManySortedSet of the carrier of S
for t being Element of (Free (S,X))
for p being Element of dom t holds t | p is Element of (Free (S,X))
let X be V6() ManySortedSet of the carrier of S; :: thesis: for t being Element of (Free (S,X))
for p being Element of dom t holds t | p is Element of (Free (S,X))
let t be Element of (Free (S,X)); :: thesis: for p being Element of dom t holds t | p is Element of (Free (S,X))
let p be Element of dom t; :: thesis: t | p is Element of (Free (S,X))
set Y = X \/ ( the carrier of S --> {0});
reconsider t = t as Term of S,(X \/ ( the carrier of S --> {0})) by Th9;
reconsider p = p as Element of dom t ;
A1: variables_in (t | p) c= variables_in t by Th33;
A2: ( the Sorts of (Free (S,X)) = 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 x being set st
( x in the carrier of S & t in (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . x ) by CARD_5:10;
then variables_in t c= X by Th18;
then variables_in (t | p) c= X by A1, PBOOLE:15;
then t | p in { q where q is Term of S,(X \/ ( the carrier of S --> {0})) : ( the_sort_of q = the_sort_of (t | p) & variables_in q c= X ) } ;
then t | p in (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . (the_sort_of (t | p)) by Def6;
hence t | p is Element of (Free (S,X)) by A2, CARD_5:10; :: thesis: verum