let S be non void Signature; :: thesis: for X being empty-yielding 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 empty-yielding 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 Th8;
reconsider p = p as Element of dom t ;
A1: variables_in (t | p) c= variables_in t by Th32;
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 Th24, PARTFUN1:def 2;
then ex x being object st
( x in the carrier of S & t in (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . x ) by CARD_5:2;
then variables_in t c= X by Th17;
then variables_in (t | p) c= X by A1, PBOOLE:13;
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 Def5;
hence t | p is Element of (Free (S,X)) by A2, CARD_5:2; :: thesis: verum