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 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 V2() ManySortedSet of the carrier of S; :: 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: 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;
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
x in V . (the_sort_of t) and
A5: 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 XTUPLE_0:1;
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
hence the_sort_of t = the_result_sort_of o by A2, A4, XTUPLE_0:1; :: thesis: verum
end;
end;