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