let A, B, C be non empty set ; :: thesis: 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
let f be Function of A,B; :: thesis: ( ( for x being Element of A holds f . x in C ) implies f is Function of A,C )
A1: dom f = A by FUNCT_2:def 1;
assume for x being Element of A holds f . x in C ; :: thesis: f is Function of A,C
then for x being set st x in A holds
f . x in C ;
hence f is Function of A,C by A1, FUNCT_2:5; :: thesis: verum