let S be non empty non void ManySortedSign ; 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; 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; 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; ( 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]
; the_sort_of t = the_result_sort_of o