let S be non empty non void ManySortedSign ; :: thesis: for V being V5() ManySortedSet of
for t being Term of S,V ex s being SortSymbol of S st t in FreeSort V,s
let V be V5() ManySortedSet of ; :: 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:47;

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 & ts = [x,s] ) by MSAFREE:7;
take s ; :: thesis: t in FreeSort V,s
t = root-tree [x,s] by A1, 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 12; :: 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
A2: nt = [o,x2] by DOMAIN_1:9;
A3: x2 = the carrier of S by TARSKI:def 1;
take s = the_result_sort_of o; :: thesis: t in FreeSort V,s
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 A2, A3;
hence t in FreeSort V,s by MSAFREE:def 12; :: thesis: verum

end;

end;