let S be non void Signature; :: thesis: for X being V9() 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 V9() 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 --> );
reconsider t = t as Term of S,(X (\/) ( the carrier of S --> )) 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 --> ))) & dom (S -Terms (X,(X (\/) ( the carrier of S --> )))) = the carrier of S ) by ;
then ex x being object st
( x in the carrier of S & t in (S -Terms (X,(X (\/) ( the carrier of S --> )))) . x ) by CARD_5:2;
then variables_in t c= X by Th17;
then variables_in (t | p) c= X by ;
then t | p in { q where q is Term of S,(X (\/) ( the carrier of S --> )) : ( 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 --> )))) . (the_sort_of (t | p)) by Def5;
hence t | p is Element of (Free (S,X)) by ; :: thesis: verum