:: deftheorem Def2 defines x". ZF_FUND1:def 3 :
for v1 being Element of VAR
for b₂ being Element of NAT holds
( b₂ = x". v1 iff x. b₂ = v1 );