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}:] ; :: thesis: verum

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}:] ; :: thesis: verum