reconsider y1 = [ the AcceptS of s,(x `1_3)] as Element of UnionSt (s,t) by Th41;
set Sym = the Symbols of s \/ the Symbols of t;
reconsider y2 = x `2_3 as Element of the Symbols of s \/ the Symbols of t by XBOOLE_0:def 3;
[y1,y2,(x `3_3)] in [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t),{(- 1),0,1}:] ;
hence [[ the AcceptS of s,(x `1_3)],(x `2_3),(x `3_3)] is Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t),{(- 1),0,1}:] ; :: thesis: verum