let S be non void Signature; :: thesis: for X being with_missing_variables ManySortedSet of the carrier of S
for t being Term of S,(X (\/) ( the carrier of S --> {0})) st t in Union the Sorts of (Free (S,X)) holds
t in the Sorts of (Free (S,X)) . (the_sort_of t)
let X be with_missing_variables ManySortedSet of the carrier of S; :: thesis: for t being Term of S,(X (\/) ( the carrier of S --> {0})) st t in Union the Sorts of (Free (S,X)) holds
t in the Sorts of (Free (S,X)) . (the_sort_of t)
set V = X (\/) ( the carrier of S --> {0});
set A = Free (S,X);
set U = the Sorts of (Free (S,X));
A1: the Sorts of (Free (S,X)) = S -Terms (X,(X (\/) ( the carrier of S --> {0}))) by MSAFREE3:24;
let t be Term of S,(X (\/) ( the carrier of S --> {0})); :: thesis: ( t in Union the Sorts of (Free (S,X)) implies t in the Sorts of (Free (S,X)) . (the_sort_of t) )
assume t in Union the Sorts of (Free (S,X)) ; :: thesis: t in the Sorts of (Free (S,X)) . (the_sort_of t)
then consider s being object such that
A2: s in dom the Sorts of (Free (S,X)) and
A3: t in the Sorts of (Free (S,X)) . s by CARD_5:2;
reconsider s = s as SortSymbol of S by A2;
the Sorts of (Free (S,X)) . s = { r where r is Term of S,(X (\/) ( the carrier of S --> {0})) : ( the_sort_of r = s & variables_in r c= X ) } by A1, MSAFREE3:def 5;
then ex r being Term of S,(X (\/) ( the carrier of S --> {0})) st
( t = r & the_sort_of r = s & variables_in r c= X ) by A3;
hence t in the Sorts of (Free (S,X)) . (the_sort_of t) by A3; :: thesis: verum