let S be OrderSortedSign; :: thesis: for X being non-empty 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 non-empty 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, XTUPLE_0:1;
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