let S be OrderSortedSign; :: thesis: for X being V5() ManySortedSet of S
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 S; :: 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
reconsider x1 = x as FinSequence of TS (DTConOSA X) by Th13;
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
OSSym o,X ==> roots x by Th13;
then consider o1 being OperSymbol of S such that
A2: OSSym o,X = [o1,the carrier of S] and
x1 in Args o1,(ParsedTermsOSA X) and
A3: (OSSym o,X) -tree x1 = (Den o1,(ParsedTermsOSA X)) . x1 and
A4: 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 Th12;
A5: o = o1 by A2, ZFMISC_1:33;
then t in the Sorts of (ParsedTermsOSA X) . (the_result_sort_of o) by A1, A3, A4;
hence LeastSort t = the_result_sort_of o by A1, A3, A4, A5, Def12; :: thesis: verum