:: deftheorem Def1 defines decode ZF_FUND1:def 2 :
for b₁ being Function of omega,VAR holds
( b₁ = decode iff for p being Element of omega holds b₁ . p = x. (card p) );