ex f being Function of NAT , NAT st
for k being Element of NAT holds f . k = Euler k from FUNCT_2:sch 4();
hence ex b₁ being Function of NAT , NAT st
for k being Element of NAT holds b₁ . k = Euler k ; :: thesis: verum