:: deftheorem Def28 defines SecondTuringSymbol TURING_1:def 28 :
for X, Y, Z being non empty set
for x being Element of [:X,(Y \/ Z):] st ex u being set ex z being Element of Z st x = [u,z] holds
SecondTuringSymbol x = x `2 ;