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