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 c being Element of X st
( c in P & y = f . c )
let f be Function of X,Y; :: thesis: for y being set st y in f .: P holds
ex c being Element of X st
( c in P & y = f . c )
let y be set ; :: thesis: ( y in f .: P implies ex c being Element of X st
( c in P & y = f . c ) )
assume y in f .: P ; :: thesis: ex c being Element of X st
( c in P & y = f . c )
then consider x being set such that
A1: x in X and
A2: x in P and
A3: y = f . x by Th115;
reconsider c = x as Element of X by A1;
take c ; :: thesis: ( c in P & y = f . c )
thus ( c in P & y = f . c ) by A2, A3; :: thesis: verum