ex f being sequence of NAT st

for k being Element of NAT holds f . k = Euler k from FUNCT_2:sch 4();

hence ex b_{1} being sequence of NAT st

for k being Element of NAT holds b_{1} . k = Euler k
; :: thesis: verum

for k being Element of NAT holds f . k = Euler k from FUNCT_2:sch 4();

hence ex b

for k being Element of NAT holds b