let f be Function; for r being Relation
for x being object holds
( x in f .: r iff ex y, z being object st
( [y,z] in r & [y,z] in dom f & f . (y,z) = x ) )
let r be Relation; for x being object holds
( x in f .: r iff ex y, z being object st
( [y,z] in r & [y,z] in dom f & f . (y,z) = x ) )
let x be object ; ( x in f .: r iff ex y, z being object st
( [y,z] in r & [y,z] in dom f & f . (y,z) = x ) )
hereby ( ex y, z being object st
( [y,z] in r & [y,z] in dom f & f . (y,z) = x ) implies x in f .: r )
assume
x in f .: r
;
ex y, z being object st
( [y,z] in r & [y,z] in dom f & f . (y,z) = x )then consider t being
object such that A1:
(
t in dom f &
t in r &
x = f . t )
by FUNCT_1:def 6;
consider y,
z being
object such that A2:
t = [y,z]
by A1, RELAT_1:def 1;
f . (
y,
z)
= f . [y,z]
;
hence
ex
y,
z being
object st
(
[y,z] in r &
[y,z] in dom f &
f . (
y,
z)
= x )
by A1, A2;
verum
end;
thus
( ex y, z being object st
( [y,z] in r & [y,z] in dom f & f . (y,z) = x ) implies x in f .: r )
by FUNCT_1:def 6; verum