let f be Function; (pr1 ((dom f),(rng f))) .: f = dom f
now for y being object holds
( ( y in dom f implies ex x being object st
( x in dom (pr1 ((dom f),(rng f))) & x in f & y = (pr1 ((dom f),(rng f))) . x ) ) & ( ex x being object st
( x in dom (pr1 ((dom f),(rng f))) & x in f & y = (pr1 ((dom f),(rng f))) . x ) implies y in dom f ) )let y be
object ;
( ( y in dom f implies ex x being object st
( x in dom (pr1 ((dom f),(rng f))) & x in f & y = (pr1 ((dom f),(rng f))) . x ) ) & ( ex x being object st
( x in dom (pr1 ((dom f),(rng f))) & x in f & y = (pr1 ((dom f),(rng f))) . x ) implies y in dom f ) )thus
(
y in dom f implies ex
x being
object st
(
x in dom (pr1 ((dom f),(rng f))) &
x in f &
y = (pr1 ((dom f),(rng f))) . x ) )
( ex x being object st
( x in dom (pr1 ((dom f),(rng f))) & x in f & y = (pr1 ((dom f),(rng f))) . x ) implies y in dom f )proof
assume A1:
y in dom f
;
ex x being object st
( x in dom (pr1 ((dom f),(rng f))) & x in f & y = (pr1 ((dom f),(rng f))) . x )
take
[y,(f . y)]
;
( [y,(f . y)] in dom (pr1 ((dom f),(rng f))) & [y,(f . y)] in f & y = (pr1 ((dom f),(rng f))) . [y,(f . y)] )
A2:
f . y in rng f
by A1, FUNCT_1:def 3;
then
[y,(f . y)] in [:(dom f),(rng f):]
by A1, ZFMISC_1:87;
hence
[y,(f . y)] in dom (pr1 ((dom f),(rng f)))
by Def4;
( [y,(f . y)] in f & y = (pr1 ((dom f),(rng f))) . [y,(f . y)] )
thus
[y,(f . y)] in f
by A1, FUNCT_1:def 2;
y = (pr1 ((dom f),(rng f))) . [y,(f . y)]
thus y =
(pr1 ((dom f),(rng f))) . (
y,
(f . y))
by A1, A2, Def4
.=
(pr1 ((dom f),(rng f))) . [y,(f . y)]
;
verum
end; given x being
object such that A3:
x in dom (pr1 ((dom f),(rng f)))
and
x in f
and A4:
y = (pr1 ((dom f),(rng f))) . x
;
y in dom fconsider x1,
x2 being
object such that A5:
(
x1 in dom f &
x2 in rng f )
and A6:
x = [x1,x2]
by A3, ZFMISC_1:84;
y = (pr1 ((dom f),(rng f))) . (
x1,
x2)
by A4, A6;
hence
y in dom f
by A5, Def4;
verum end;
hence
(pr1 ((dom f),(rng f))) .: f = dom f
by FUNCT_1:def 6; verum