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:25;
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 set 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:10;
reconsider s = s as SortSymbol of S by A2, 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 A3;
hence t is Term of S,(X \/ (the carrier of S --> {0 })) ; :: thesis: verum