let S be OrderSortedSign; :: thesis: for X being V5() ManySortedSet of
for t being Element of TS (DTConOSA X)
for o being OperSymbol of S st t . {} = [o,the carrier of S] holds
( ex p being SubtreeSeq of OSSym o,X st
( t = (OSSym o,X) -tree p & OSSym o,X ==> roots p & p in Args o,(ParsedTermsOSA X) & t = (Den o,(ParsedTermsOSA X)) . p ) & ( for s2 being Element of S
for x being set holds t <> root-tree [x,s2] ) & ( for s1 being Element of S holds
( t in the Sorts of (ParsedTermsOSA X) . s1 iff the_result_sort_of o <= s1 ) ) )
let X be V5() ManySortedSet of ; :: thesis: for t being Element of TS (DTConOSA X)
for o being OperSymbol of S st t . {} = [o,the carrier of S] holds
( ex p being SubtreeSeq of OSSym o,X st
( t = (OSSym o,X) -tree p & OSSym o,X ==> roots p & p in Args o,(ParsedTermsOSA X) & t = (Den o,(ParsedTermsOSA X)) . p ) & ( for s2 being Element of S
for x being set holds t <> root-tree [x,s2] ) & ( for s1 being Element of S holds
( t in the Sorts of (ParsedTermsOSA X) . s1 iff the_result_sort_of o <= s1 ) ) )
let t be Element of TS (DTConOSA X); :: thesis: for o being OperSymbol of S st t . {} = [o,the carrier of S] holds
( ex p being SubtreeSeq of OSSym o,X st
( t = (OSSym o,X) -tree p & OSSym o,X ==> roots p & p in Args o,(ParsedTermsOSA X) & t = (Den o,(ParsedTermsOSA X)) . p ) & ( for s2 being Element of S
for x being set holds t <> root-tree [x,s2] ) & ( for s1 being Element of S holds
( t in the Sorts of (ParsedTermsOSA X) . s1 iff the_result_sort_of o <= s1 ) ) )
let o be OperSymbol of S; :: thesis: ( t . {} = [o,the carrier of S] implies ( ex p being SubtreeSeq of OSSym o,X st
( t = (OSSym o,X) -tree p & OSSym o,X ==> roots p & p in Args o,(ParsedTermsOSA X) & t = (Den o,(ParsedTermsOSA X)) . p ) & ( for s2 being Element of S
for x being set holds t <> root-tree [x,s2] ) & ( for s1 being Element of S holds
( t in the Sorts of (ParsedTermsOSA X) . s1 iff the_result_sort_of o <= s1 ) ) ) )
assume A1: t . {} = [o,the carrier of S] ; :: thesis: ( ex p being SubtreeSeq of OSSym o,X st
( t = (OSSym o,X) -tree p & OSSym o,X ==> roots p & p in Args o,(ParsedTermsOSA X) & t = (Den o,(ParsedTermsOSA X)) . p ) & ( for s2 being Element of S
for x being set holds t <> root-tree [x,s2] ) & ( for s1 being Element of S holds
( t in the Sorts of (ParsedTermsOSA X) . s1 iff the_result_sort_of o <= s1 ) ) )
set G = DTConOSA X;
set PTA = ParsedTermsOSA X;
reconsider SPTA = the Sorts of (ParsedTermsOSA X) as OrderSortedSet of ;
consider p being FinSequence of TS (DTConOSA X) such that
A2: ( t = (OSSym o,X) -tree p & OSSym o,X ==> roots p ) by A1, DTCONSTR:10;
reconsider p = p as SubtreeSeq of OSSym o,X by A2, DTCONSTR:def 9;
p in (((ParsedTerms X) # ) * the Arity of S) . o by A2, Th7;
then A3: p in Args o,(ParsedTermsOSA X) by MSUALG_1:def 9;
(Den o,(ParsedTermsOSA X)) . p = (the Charact of (ParsedTermsOSA X) . o) . p by MSUALG_1:def 11
.= (PTDenOp o,X) . p by Def10
.= t by A2, Def9 ;
hence ex p being SubtreeSeq of OSSym o,X st
( t = (OSSym o,X) -tree p & OSSym o,X ==> roots p & p in Args o,(ParsedTermsOSA X) & t = (Den o,(ParsedTermsOSA X)) . p ) by A2, A3; :: thesis: ( ( for s2 being Element of S
for x being set holds t <> root-tree [x,s2] ) & ( for s1 being Element of S holds
( t in the Sorts of (ParsedTermsOSA X) . s1 iff the_result_sort_of o <= s1 ) ) )
set s = the_result_sort_of o;
t in { a where a is Element of TS (DTConOSA X) : ( ex s1 being Element of S ex x being set st
( s1 <= the_result_sort_of o & 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 <= the_result_sort_of o ) ) } by A1;
then A4: t in SPTA . (the_result_sort_of o) by Th9;
thus A5: for s2 being Element of S
for x being set holds t <> root-tree [x,s2] :: thesis: for s1 being Element of S holds
( t in the Sorts of (ParsedTermsOSA X) . s1 iff the_result_sort_of o <= s1 )

proof

let s2 be Element of S; :: thesis: for x being set holds t <> root-tree [x,s2]
let x be set ; :: thesis: t <> root-tree [x,s2]
assume t = root-tree [x,s2] ; :: thesis: contradiction
then [x,s2] = [o,the carrier of S] by A1, TREES_4:3;
then s2 = the carrier of S by ZFMISC_1:33;
then s2 in s2 ;
hence contradiction ; :: thesis: verum

end;

let s1 be Element of S; :: thesis: ( t in the Sorts of (ParsedTermsOSA X) . s1 iff the_result_sort_of o <= s1 )
reconsider s0 = the_result_sort_of o, s11 = s1 as Element of S ;

hereby :: thesis: ( the_result_sort_of o <= s1 implies t in the Sorts of (ParsedTermsOSA X) . s1 )

assume t in the Sorts of (ParsedTermsOSA X) . s1 ; :: thesis: the_result_sort_of o <= s1
then t in { a where a is Element of TS (DTConOSA X) : ( ex s2 being Element of S ex x being set st
( s2 <= s1 & x in X . s2 & a = root-tree [x,s2] ) or ex o being OperSymbol of S st
( [o,the carrier of S] = a . {} & the_result_sort_of o <= s1 ) ) } by Th9;
then consider a being Element of TS (DTConOSA X) such that
A6: a = t and
A7: ( ex s2 being Element of S ex x being set st
( s2 <= s1 & x in X . s2 & a = root-tree [x,s2] ) or ex o being OperSymbol of S st
( [o,the carrier of S] = a . {} & the_result_sort_of o <= s1 ) ) ;
consider o1 being OperSymbol of S such that
A8: ( [o1,the carrier of S] = a . {} & the_result_sort_of o1 <= s1 ) by A5, A6, A7;
thus the_result_sort_of o <= s1 by A1, A6, A8, ZFMISC_1:33; :: thesis: verum

end;

assume the_result_sort_of o <= s1 ; :: thesis: t in the Sorts of (ParsedTermsOSA X) . s1
then SPTA . s0 c= SPTA . s11 by OSALG_1:def 18;
hence t in the Sorts of (ParsedTermsOSA X) . s1 by A4; :: thesis: verum