:: deftheorem defines id TURING_1:def 10 :
for A, B being non empty set
for y being set st y in B holds
for b₄ being Function of A,[:A,B:] holds
( b₄ = id (A,B,y) iff for x being Element of A holds b₄ . x = [x,y] );