let X, Y, P be set ; :: thesis: for f being Function of X,Y
for y being set st y in f .: P holds
ex x being set st
( x in X & x in P & y = f . x )
let f be Function of X,Y; :: thesis: for y being set st y in f .: P holds
ex x being set st
( x in X & x in P & y = f . x )
let y be set ; :: thesis: ( y in f .: P implies ex x being set st
( x in X & x in P & y = f . x ) )
assume y in f .: P ; :: thesis: ex x being set st
( x in X & x in P & y = f . x )
then consider x being set such that
A1: x in dom f and
A2: ( x in P & y = f . x ) by FUNCT_1:def 12;
take x ; :: thesis: ( x in X & x in P & y = f . x )
thus x in X by A1; :: thesis: ( x in P & y = f . x )
thus ( x in P & y = f . x ) by A2; :: thesis: verum