:: deftheorem Def30 defines UnionTran TURING_1:def 30 :
for s, t being TuringStr
for b₃ being Function of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t):],[:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t),{(- 1),0,1}:] holds
( b₃ = UnionTran (s,t) iff for x being Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t):] holds b₃ . x = Uniontran (s,t,x) );