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 --> {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

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 --> {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