let y be object ; :: thesis:
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 ) ) :: thesis:

assume A1: y in dom f ; :: thesis:
take [y,(f . y)] ; :: thesis:
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; :: thesis:
thus [y,(f . y)] in f by A1, FUNCT_1:def 2; :: thesis:
thus y = (pr1 ((dom f),(rng f))) . (y,(f . y)) by A1, A2, Def4
.= (pr1 ((dom f),(rng f))) . [y,(f . y)] ; :: thesis:

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 ; :: thesis:
consider 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; :: thesis:

end;