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

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