:: deftheorem Def7 defines Euler_phi NAT_5:def 7 :
for b₁ being sequence of NAT holds
( b₁ = Euler_phi iff for k being Element of NAT holds b₁ . k = Euler k );