let S be non empty non void ManySortedSign ; :: thesis: for V being V5() ManySortedSet of
for t being Term of S,V
for o being OperSymbol of S st t . {} = [o,the carrier of S] holds
the_sort_of t = the_result_sort_of o
let V be V5() ManySortedSet of ; :: thesis: for t being Term of S,V
for o being OperSymbol of S st t . {} = [o,the carrier of S] holds
the_sort_of t = the_result_sort_of o
let t be Term of S,V; :: thesis: for o being OperSymbol of S st t . {} = [o,the carrier of S] holds
the_sort_of t = the_result_sort_of o
let o be OperSymbol of S; :: thesis: ( t . {} = [o,the carrier of S] implies the_sort_of t = the_result_sort_of o )
set X = V;
set G = DTConMSA V;
set tst = the_sort_of t;
A1: t in FreeSort V,(the_sort_of t) by Def5;
FreeSort V,(the_sort_of t) = { a where a is Element of TS (DTConMSA V) : ( ex x being set st
( x in V . (the_sort_of t) & a = root-tree [x,(the_sort_of t)] ) or ex o being OperSymbol of S st
( [o,the carrier of S] = a . {} & the_result_sort_of o = the_sort_of t ) ) } by MSAFREE:def 12;
then consider a being Element of TS (DTConMSA V) such that
A2: t = a and
A3: ( ex x being set st
( x in V . (the_sort_of t) & a = root-tree [x,(the_sort_of t)] ) or ex o being OperSymbol of S st
( [o,the carrier of S] = a . {} & the_result_sort_of o = the_sort_of t ) ) by A1;
assume A4: t . {} = [o,the carrier of S] ; :: thesis: the_sort_of t = the_result_sort_of o

per cases ( ex x being set st
( x in V . (the_sort_of t) & a = root-tree [x,(the_sort_of t)] ) or ex o being OperSymbol of S st
( [o,the carrier of S] = a . {} & the_result_sort_of o = the_sort_of t ) ) by A3;

suppose ex x being set st
( x in V . (the_sort_of t) & a = root-tree [x,(the_sort_of t)] ) ; :: thesis: the_sort_of t = the_result_sort_of o

then consider x being set such that
A5: ( x in V . (the_sort_of t) & a = root-tree [x,(the_sort_of t)] ) ;
[o,the carrier of S] = [x,(the_sort_of t)] by A2, A4, A5, TREES_4:3;
then the carrier of S = the_sort_of t by ZFMISC_1:33;
hence the_sort_of t = the_result_sort_of o by Lm7; :: thesis: verum

end;

suppose ex o being OperSymbol of S st
( [o,the carrier of S] = a . {} & the_result_sort_of o = the_sort_of t ) ; :: thesis: the_sort_of t = the_result_sort_of o

then consider o' being OperSymbol of S such that
A6: ( [o',the carrier of S] = a . {} & the_result_sort_of o' = the_sort_of t ) ;
thus the_sort_of t = the_result_sort_of o by A2, A4, A6, ZFMISC_1:33; :: thesis: verum

end;

end;