reconsider y1 = [(x `1_3), the InitS of t] as Element of UnionSt (s,t) by Th40;
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
[[(x `1_3), the InitS of t],(x `2_3),(x `3_3)] is Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t),{(- 1),0,1}:]
; verum