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