let S be locally_directed OrderSortedSign; for X being V2() ManySortedSet of S
for x, y, s being object st [x,s] in (PTClasses X) . y holds
( x in TS (DTConOSA X) & y in TS (DTConOSA X) & s in the carrier of S )
let X be V2() ManySortedSet of S; for x, y, s being object st [x,s] in (PTClasses X) . y holds
( x in TS (DTConOSA X) & y in TS (DTConOSA X) & s in the carrier of S )
set D = DTConOSA X;
set F = PTClasses X;
A1:
rng (PTClasses X) c= bool [:(TS (DTConOSA X)), the carrier of S:]
by RELAT_1:def 19;
let x, y, s be object ; ( [x,s] in (PTClasses X) . y implies ( x in TS (DTConOSA X) & y in TS (DTConOSA X) & s in the carrier of S ) )
assume A2:
[x,s] in (PTClasses X) . y
; ( x in TS (DTConOSA X) & y in TS (DTConOSA X) & s in the carrier of S )
A3:
y in TS (DTConOSA X)
dom (PTClasses X) = TS (DTConOSA X)
by FUNCT_2:def 1;
then
(PTClasses X) . y in rng (PTClasses X)
by A3, FUNCT_1:3;
hence
( x in TS (DTConOSA X) & y in TS (DTConOSA X) & s in the carrier of S )
by A2, A1, A3, ZFMISC_1:87; verum