let y be object ; :: thesis: for A, B being set
for f being Function of A,B st y in rng f holds
ex x being Element of A st y = f . x
let A, B be set ; :: thesis: for f being Function of A,B st y in rng f holds
ex x being Element of A st y = f . x
let f be Function of A,B; :: thesis: ( y in rng f implies ex x being Element of A st y = f . x )
assume y in rng f ; :: thesis: ex x being Element of A st y = f . x
then consider x being object such that
A1: x in A and
A2: f . x = y by Th11;
reconsider x = x as Element of A by A1;
take x ; :: thesis: y = f . x
thus y = f . x by A2; :: thesis: verum