let S be non void Signature; :: thesis: for X being with_missing_variables ManySortedSet of the carrier of S
for t being set st t in Union the Sorts of (Free (S,X)) holds
t is Term of S,(X (\/) ( the carrier of S --> {0}))
let X be with_missing_variables ManySortedSet of the carrier of S; :: thesis: for t being set st t in Union the Sorts of (Free (S,X)) holds
t is Term of S,(X (\/) ( the carrier of S --> {0}))
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 set ; :: thesis: ( t in Union the Sorts of (Free (S,X)) implies t is Term of S,(X (\/) ( the carrier of S --> {0})) )
assume t in Union the Sorts of (Free (S,X)) ; :: thesis: t is Term of S,(X (\/) ( the carrier of S --> {0}))
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 is Term of S,(X (\/) ( the carrier of S --> {0})) ; :: thesis: verum