let A be set ; :: thesis: ex F being Function of NAT,{A} st
for n being Element of NAT holds F . n = A
take NAT --> A ; :: thesis: for n being Element of NAT holds (NAT --> A) . n = A
thus for n being Element of NAT holds (NAT --> A) . n = A by TARSKI:def 1; :: thesis: verum