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 ;
TARSKI:def 3 ( 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 ) ) ) }
;
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;
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:]
; verum