theorem Th1: :: HEYTING1:1

for A, B, C being non empty set
for f being Function of A,B st ( for x being Element of A holds f . x in C ) holds
f is Function of A,C