let X, Y, P be set ; :: thesis: for f being Function of X,Y
for y being object st y in f .: P holds
ex x being object st
( x in X & x in P & y = f . x )
let f be Function of X,Y; :: thesis: for y being object st y in f .: P holds
ex x being object st
( x in X & x in P & y = f . x )
let y be object ; :: thesis: ( y in f .: P implies ex x being object st
( x in X & x in P & y = f . x ) )
assume y in f .: P ; :: thesis: ex x being object st
( x in X & x in P & y = f . x )
then consider x being object such that
A1: x in dom f and
A2: ( x in P & y = f . x ) by FUNCT_1:def 6;
reconsider x = x as set by TARSKI:1;
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