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