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