let f be Function; :: thesis: for r being Relation
for x being set holds
( x in f .: r iff ex y, z being set st
( [y,z] in r & [y,z] in dom f & f . (y,z) = x ) )
let r be Relation; :: thesis: for x being set holds
( x in f .: r iff ex y, z being set st
( [y,z] in r & [y,z] in dom f & f . (y,z) = x ) )
let x be set ; :: thesis: ( x in f .: r iff ex y, z being set st
( [y,z] in r & [y,z] in dom f & f . (y,z) = x ) )

hereby :: thesis: ( ex y, z being set st
( [y,z] in r & [y,z] in dom f & f . (y,z) = x ) implies x in f .: r )

assume x in f .: r ; :: thesis: ex y, z being set st
( [y,z] in r & [y,z] in dom f & f . (y,z) = x )
then consider t being set such that
A1: ( t in dom f & t in r & x = f . t ) by FUNCT_1:def 6;
consider y, z being set such that
A2: t = [y,z] by A1, RELAT_1:def 1;
f . (y,z) = f . [y,z] ;
hence ex y, z being set st
( [y,z] in r & [y,z] in dom f & f . (y,z) = x ) by A1, A2; :: thesis: verum

end;

thus ( ex y, z being set st
( [y,z] in r & [y,z] in dom f & f . (y,z) = x ) implies x in f .: r ) by FUNCT_1:def 6; :: thesis: verum