let S be OrderSortedSign; :: thesis: for X being non-empty ManySortedSet of S
for s being Element of S
for x being set st x in the Sorts of (ParsedTermsOSA X) . s holds
x is Element of TS (DTConOSA X)
let X be non-empty ManySortedSet of S; :: thesis: for s being Element of S
for x being set st x in the Sorts of (ParsedTermsOSA X) . s holds
x is Element of TS (DTConOSA X)
let s be Element of S; :: thesis: for x being set st x in the Sorts of (ParsedTermsOSA X) . s holds
x is Element of TS (DTConOSA X)
let x be set ; :: thesis: ( x in the Sorts of (ParsedTermsOSA X) . s implies x is Element of TS (DTConOSA X) )
assume A1: x in the Sorts of (ParsedTermsOSA X) . s ; :: thesis: x is Element of TS (DTConOSA X)
set PTA = ParsedTermsOSA X;
set SPTA = the Sorts of (ParsedTermsOSA X);
s in the carrier of S ;
then s in dom the Sorts of (ParsedTermsOSA X) by PARTFUN1:def 2;
then the Sorts of (ParsedTermsOSA X) . s in rng the Sorts of (ParsedTermsOSA X) by FUNCT_1:def 3;
then x in union (rng the Sorts of (ParsedTermsOSA X)) by A1, TARSKI:def 4;
then reconsider x1 = x as Element of Union the Sorts of (ParsedTermsOSA X) by CARD_3:def 4;
x1 is Element of (ParsedTermsOSA X) ;
hence x is Element of TS (DTConOSA X) by Th14; :: thesis: verum