let S be non void Signature; :: thesis: for X being with_missing_variables ManySortedSet of
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 ; :: 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:25;
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 set such that
Z1: ( s in dom the Sorts of (Free S,X) & t in the Sorts of (Free S,X) . s ) by CARD_5:10;
reconsider s = s as SortSymbol of S by Z1, PARTFUN1:def 4;
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 6;
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 Z1;
hence t in the Sorts of (Free S,X) . (the_sort_of t) by Z1; :: thesis: verum