set MySigmatau = { A where A is Element of Sigma : for t2 being Element of S holds A /\ { w where w is Element of Omega : tau . w <= t2 } in MyFunc . t2 } ;
A1 . n inrng A1
byFUNCT_2:4, ORDINAL1:def 12; then
A1 . n in { A where A is Element of Sigma : for t2 being Element of S holds A /\ { w where w is Element of Omega : tau . w <= t2 } in MyFunc . t2 } byLOC1; then consider B being Element of Sigma such that GW1:
( A1 . n = B & ( for t2 being Element of S holds B /\ { w where w is Element of Omega : tau . w <= t2 } in MyFunc . t2 ) )
; reconsider A1n = A1 . n as Element of Sigma byGW1; GW2:
for t being Element of S holds ((A1 . n)`)/\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t