let Z be set ; :: thesis: for A, B being non empty set
for f being Function of A,B st ( for x being Element of A holds f . x in Z ) holds
rng f c= Z
let A, B be non empty set ; :: thesis: for f being Function of A,B st ( for x being Element of A holds f . x in Z ) holds
rng f c= Z
let f be Function of A,B; :: thesis: ( ( for x being Element of A holds f . x in Z ) implies rng f c= Z )
assume A1: for x being Element of A holds f . x in Z ; :: thesis: rng f c= Z
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in Z )
assume y in rng f ; :: thesis: y in Z
then ex x being Element of A st f . x = y by Th190;
hence y in Z by A1; :: thesis: verum