let S be non empty non void ManySortedSign ; :: thesis: for V being V2() ManySortedSet of the carrier of S
for t being Term of S,V
for s being SortSymbol of S
for v being Element of V . s st t = root-tree [v,s] holds
the_sort_of t = s
let V be V2() ManySortedSet of the carrier of S; :: thesis: for t being Term of S,V
for s being SortSymbol of S
for v being Element of V . s st t = root-tree [v,s] holds
the_sort_of t = s
let t be Term of S,V; :: thesis: for s being SortSymbol of S
for v being Element of V . s st t = root-tree [v,s] holds
the_sort_of t = s
let s be SortSymbol of S; :: thesis: for v being Element of V . s st t = root-tree [v,s] holds
the_sort_of t = s
let x be Element of V . s; :: thesis: ( t = root-tree [x,s] implies the_sort_of t = s )
set X = V;
set G = DTConMSA V;
set tst = the_sort_of t;
A1: 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 10;
t in FreeSort (V,(the_sort_of t)) by Def5;
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;
A4: [x,s] in Terminals (DTConMSA V) by Lm3;
assume A5: t = root-tree [x,s] ; :: thesis: the_sort_of t = s
then t . {} = [x,s] by TREES_4:3;
then t . {} is not NonTerminal of (DTConMSA V) by A4, Lm6;
then A6: not t . {} in [: the carrier' of S,{ the carrier of S}:] by Lm5;
the carrier of S in { the carrier of S} by TARSKI:def 1;
then consider y being set such that
y in V . (the_sort_of t) and
A7: a = root-tree [y,(the_sort_of t)] by A2, A3, A6, ZFMISC_1:87;
[y,(the_sort_of t)] = [x,s] by A2, A5, A7, TREES_4:4;
hence the_sort_of t = s by XTUPLE_0:1; :: thesis: verum