let S be OrderSortedSign; :: thesis: for X being V5() ManySortedSet of
for o being OperSymbol of S
for x being Element of Args o,(ParsedTermsOSA X)
for t being Element of TS (DTConOSA X) st t = (Den o,(ParsedTermsOSA X)) . x holds
LeastSort t = the_result_sort_of o
let X be V5() ManySortedSet of ; :: thesis: for o being OperSymbol of S
for x being Element of Args o,(ParsedTermsOSA X)
for t being Element of TS (DTConOSA X) st t = (Den o,(ParsedTermsOSA X)) . x holds
LeastSort t = the_result_sort_of o
let o be OperSymbol of S; :: thesis: for x being Element of Args o,(ParsedTermsOSA X)
for t being Element of TS (DTConOSA X) st t = (Den o,(ParsedTermsOSA X)) . x holds
LeastSort t = the_result_sort_of o
let x be Element of Args o,(ParsedTermsOSA X); :: thesis: for t being Element of TS (DTConOSA X) st t = (Den o,(ParsedTermsOSA X)) . x holds
LeastSort t = the_result_sort_of o
set PTA = ParsedTermsOSA X;
let t be Element of TS (DTConOSA X); :: thesis: ( t = (Den o,(ParsedTermsOSA X)) . x implies LeastSort t = the_result_sort_of o )
assume A1: t = (Den o,(ParsedTermsOSA X)) . x ; :: thesis: LeastSort t = the_result_sort_of o
A2: ( x is FinSequence of TS (DTConOSA X) & OSSym o,X ==> roots x ) by Th13;
reconsider x1 = x as FinSequence of TS (DTConOSA X) by Th13;
consider o1 being OperSymbol of S such that
A3: ( OSSym o,X = [o1,the carrier of S] & x1 in Args o1,(ParsedTermsOSA X) & (OSSym o,X) -tree x1 = (Den o1,(ParsedTermsOSA X)) . x1 & ( for s1 being Element of S holds
( (OSSym o,X) -tree x1 in the Sorts of (ParsedTermsOSA X) . s1 iff the_result_sort_of o1 <= s1 ) ) ) by A2, Th12;
A4: o = o1 by A3, ZFMISC_1:33;
then t in the Sorts of (ParsedTermsOSA X) . (the_result_sort_of o) by A1, A3;
hence LeastSort t = the_result_sort_of o by A1, A3, A4, Def12; :: thesis: verum