set NT = { [((Den (o2,(ParsedTermsOSA X))) . x2),s3] where o2 is OperSymbol of S, x2 is Element of Args (o2,(ParsedTermsOSA X)), s3 is Element of S : ( ex o1 being OperSymbol of S st
( nt = [o1, the carrier of S] & o1 ~= o2 & len (the_arity_of o1) = len (the_arity_of o2) & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) & ex w3 being Element of the carrier of S * st
( dom w3 = dom x & ( for y being Nat st y in dom x holds
[(x2 . y),(w3 /. y)] in x . y ) ) ) } ;
{ [((Den (o2,(ParsedTermsOSA X))) . x2),s3] where o2 is OperSymbol of S, x2 is Element of Args (o2,(ParsedTermsOSA X)), s3 is Element of S : ( ex o1 being OperSymbol of S st
( nt = [o1, the carrier of S] & o1 ~= o2 & len (the_arity_of o1) = len (the_arity_of o2) & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) & ex w3 being Element of the carrier of S * st
( dom w3 = dom x & ( for y being Nat st y in dom x holds
[(x2 . y),(w3 /. y)] in x . y ) ) ) } c= [:(TS (DTConOSA X)), the carrier of S:]

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { [((Den (o2,(ParsedTermsOSA X))) . x2),s3] where o2 is OperSymbol of S, x2 is Element of Args (o2,(ParsedTermsOSA X)), s3 is Element of S : ( ex o1 being OperSymbol of S st
( nt = [o1, the carrier of S] & o1 ~= o2 & len (the_arity_of o1) = len (the_arity_of o2) & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) & ex w3 being Element of the carrier of S * st
( dom w3 = dom x & ( for y being Nat st y in dom x holds
[(x2 . y),(w3 /. y)] in x . y ) ) ) } or y in [:(TS (DTConOSA X)), the carrier of S:] )
assume y in { [((Den (o2,(ParsedTermsOSA X))) . x2),s3] where o2 is OperSymbol of S, x2 is Element of Args (o2,(ParsedTermsOSA X)), s3 is Element of S : ( ex o1 being OperSymbol of S st
( nt = [o1, the carrier of S] & o1 ~= o2 & len (the_arity_of o1) = len (the_arity_of o2) & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) & ex w3 being Element of the carrier of S * st
( dom w3 = dom x & ( for y being Nat st y in dom x holds
[(x2 . y),(w3 /. y)] in x . y ) ) ) } ; :: thesis: y in [:(TS (DTConOSA X)), the carrier of S:]
then consider o2 being OperSymbol of S, x2 being Element of Args (o2,(ParsedTermsOSA X)), s3 being Element of S such that
A1: y = [((Den (o2,(ParsedTermsOSA X))) . x2),s3] and
ex o1 being OperSymbol of S st
( nt = [o1, the carrier of S] & o1 ~= o2 & len (the_arity_of o1) = len (the_arity_of o2) & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) and
ex w3 being Element of the carrier of S * st
( dom w3 = dom x & ( for y being Nat st y in dom x holds
[(x2 . y),(w3 /. y)] in x . y ) ) ;
A2: OSSym (o2,X) ==> roots x2 by Th13;
A3: x2 is FinSequence of TS (DTConOSA X) by Th13;
then A4: (OSSym (o2,X)) -tree x2 in TS (DTConOSA X) by A2, Th12;
consider o being OperSymbol of S such that
A5: OSSym (o2,X) = [o, the carrier of S] and
x2 in Args (o,(ParsedTermsOSA X)) and
A6: (OSSym (o2,X)) -tree x2 = (Den (o,(ParsedTermsOSA X))) . x2 and
for s1 being Element of S holds
( (OSSym (o2,X)) -tree x2 in the Sorts of (ParsedTermsOSA X) . s1 iff the_result_sort_of o <= s1 ) by A3, A2, Th12;
o2 = o by A5, XTUPLE_0:1;
hence y in [:(TS (DTConOSA X)), the carrier of S:] by A1, A4, A6, ZFMISC_1:def 2; :: thesis: verum

end;

hence { [((Den (o2,(ParsedTermsOSA X))) . x2),s3] where o2 is OperSymbol of S, x2 is Element of Args (o2,(ParsedTermsOSA X)), s3 is Element of S : ( ex o1 being OperSymbol of S st
( nt = [o1, the carrier of S] & o1 ~= o2 & len (the_arity_of o1) = len (the_arity_of o2) & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) & ex w3 being Element of the carrier of S * st
( dom w3 = dom x & ( for y being Nat st y in dom x holds
[(x2 . y),(w3 /. y)] in x . y ) ) ) } is Subset of [:(TS (DTConOSA X)), the carrier of S:] ; :: thesis: verum