let S be non empty non void ManySortedSign ; :: thesis: for V being non-empty ManySortedSet of the carrier of S
for t being Term of S,V ex s being SortSymbol of S st t in FreeSort (V,s)
let V be non-empty ManySortedSet of the carrier of S; :: thesis: for t being Term of S,V ex s being SortSymbol of S st t in FreeSort (V,s)
let t be Term of S,V; :: thesis: ex s being SortSymbol of S st t in FreeSort (V,s)
set X = V;
set G = DTConMSA V;
reconsider e = {} as Node of t by TREES_1:22;

per cases ( t . {} is Terminal of (DTConMSA V) or not t . {} is Terminal of (DTConMSA V) ) ;

suppose t . {} is Terminal of (DTConMSA V) ; :: thesis: ex s being SortSymbol of S st t in FreeSort (V,s)

then reconsider ts = t . {} as Terminal of (DTConMSA V) ;
consider s being SortSymbol of S, x being set such that
A1: x in V . s and
A2: ts = [x,s] by MSAFREE:7;
take s ; :: thesis: t in FreeSort (V,s)
t = root-tree [x,s] by A2, DTCONSTR:9;
then t in { a where a is Element of TS (DTConMSA V) : ( ex x being set st
( x in V . s & a = root-tree [x,s] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = s ) ) } by A1;
hence t in FreeSort (V,s) by MSAFREE:def 10; :: thesis: verum

end;

suppose t . {} is not Terminal of (DTConMSA V) ; :: thesis: ex s being SortSymbol of S st t in FreeSort (V,s)

then reconsider nt = t . e as NonTerminal of (DTConMSA V) by Lm6;
nt in [: the carrier' of S,{ the carrier of S}:] by Lm5;
then consider o being OperSymbol of S, x2 being Element of { the carrier of S} such that
A3: nt = [o,x2] by DOMAIN_1:1;
take s = the_result_sort_of o; :: thesis: t in FreeSort (V,s)
x2 = the carrier of S by TARSKI:def 1;
then t in { a where a is Element of TS (DTConMSA V) : ( ex x being set st
( x in V . s & a = root-tree [x,s] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = s ) ) } by A3;
hence t in FreeSort (V,s) by MSAFREE:def 10; :: thesis: verum

end;

end;