let S be OrderSortedSign; :: thesis: for X being V5() ManySortedSet of
for s being Element of S holds the Sorts of (ParsedTermsOSA X) . s = { a where a is Element of TS (DTConOSA X) : ( ex s1 being Element of S ex x being set st
( s1 <= s & x in X . s1 & a = root-tree [x,s1] ) or ex o being OperSymbol of S st
( [o,the carrier of S] = a . {} & the_result_sort_of o <= s ) ) }
let X be V5() ManySortedSet of ; :: thesis: for s being Element of S holds the Sorts of (ParsedTermsOSA X) . s = { a where a is Element of TS (DTConOSA X) : ( ex s1 being Element of S ex x being set st
( s1 <= s & x in X . s1 & a = root-tree [x,s1] ) or ex o being OperSymbol of S st
( [o,the carrier of S] = a . {} & the_result_sort_of o <= s ) ) }
let s be Element of S; :: thesis: the Sorts of (ParsedTermsOSA X) . s = { a where a is Element of TS (DTConOSA X) : ( ex s1 being Element of S ex x being set st
( s1 <= s & x in X . s1 & a = root-tree [x,s1] ) or ex o being OperSymbol of S st
( [o,the carrier of S] = a . {} & the_result_sort_of o <= s ) ) }
set PTA = ParsedTermsOSA X;
{ a where a is Element of TS (DTConOSA X) : ( ex s1 being Element of S ex x being set st
( s1 <= s & x in X . s1 & a = root-tree [x,s1] ) or ex o being OperSymbol of S st
( [o,the carrier of S] = a . {} & the_result_sort_of o <= s ) ) } = ParsedTerms X,s
.= the Sorts of (ParsedTermsOSA X) . s by Def8 ;
hence the Sorts of (ParsedTermsOSA X) . s = { a where a is Element of TS (DTConOSA X) : ( ex s1 being Element of S ex x being set st
( s1 <= s & x in X . s1 & a = root-tree [x,s1] ) or ex o being OperSymbol of S st
( [o,the carrier of S] = a . {} & the_result_sort_of o <= s ) ) } ; :: thesis: verum