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 )
assume for x being Element of A holds f . x in C ; :: thesis: f is Function of A,C
then ( dom f = A & ( for x being object st x in A holds
f . x in C ) ) by FUNCT_2:def 1;
hence f is Function of A,C by FUNCT_2:3; :: thesis: verum