let f be Function; :: thesis: ( f is one-to-one implies for g being Function holds
( g = f " iff ( dom g = rng f & ( for y, x being set holds
( y in rng f & x = g . y iff ( x in dom f & y = f . x ) ) ) ) ) )
assume A1: f is one-to-one ; :: thesis: for g being Function holds
( g = f " iff ( dom g = rng f & ( for y, x being set holds
( y in rng f & x = g . y iff ( x in dom f & y = f . x ) ) ) ) )
let g be Function; :: thesis: ( g = f " iff ( dom g = rng f & ( for y, x being set holds
( y in rng f & x = g . y iff ( x in dom f & y = f . x ) ) ) ) )
thus ( g = f " implies ( dom g = rng f & ( for y, x being set holds
( y in rng f & x = g . y iff ( x in dom f & y = f . x ) ) ) ) ) :: thesis: ( dom g = rng f & ( for y, x being set holds
( y in rng f & x = g . y iff ( x in dom f & y = f . x ) ) ) implies g = f " )

proof

assume g = f " ; :: thesis: ( dom g = rng f & ( for y, x being set holds
( y in rng f & x = g . y iff ( x in dom f & y = f . x ) ) ) )
then A2: g = f ~ by A1, Def9;
hence dom g = rng f by RELAT_1:37; :: thesis: for y, x being set holds
( y in rng f & x = g . y iff ( x in dom f & y = f . x ) )
let y, x be set ; :: thesis: ( y in rng f & x = g . y iff ( x in dom f & y = f . x ) )
thus ( y in rng f & x = g . y implies ( x in dom f & y = f . x ) ) :: thesis: ( x in dom f & y = f . x implies ( y in rng f & x = g . y ) )

proof

assume that
A3: y in rng f and
A4: x = g . y ; :: thesis: ( x in dom f & y = f . x )
y in dom g by A2, A3, RELAT_1:37;
then [y,x] in g by A4, Def4;
then A5: [x,y] in f by A2, RELAT_1:def 7;
hence x in dom f by RELAT_1:def 4; :: thesis: y = f . x
hence y = f . x by A5, Def4; :: thesis: verum

end;

assume that
A6: x in dom f and
A7: y = f . x ; :: thesis: ( y in rng f & x = g . y )
A8: [x,y] in f by A6, A7, Def4;
hence y in rng f by RELAT_1:def 5; :: thesis: x = g . y
then A9: y in dom g by A2, RELAT_1:37;
[y,x] in g by A2, A8, RELAT_1:def 7;
hence x = g . y by A9, Def4; :: thesis: verum

end;

assume that
A10: dom g = rng f and
A11: for y, x being set holds
( y in rng f & x = g . y iff ( x in dom f & y = f . x ) ) ; :: thesis: g = f "
let a, b be set ; :: according to RELAT_1:def 2 :: thesis: ( ( not [a,b] in g or [a,b] in f " ) & ( not [a,b] in f " or [a,b] in g ) )
thus ( [a,b] in g implies [a,b] in f " ) :: thesis: ( not [a,b] in f " or [a,b] in g )

proof

assume A12: [a,b] in g ; :: thesis: [a,b] in f "
then a in dom g by RELAT_1:def 4;
then ( a in rng f & b = g . a ) by A10, A12, Def4;
then ( b in dom f & a = f . b ) by A11;
then [b,a] in f by Def4;
then [a,b] in f ~ by RELAT_1:def 7;
hence [a,b] in f " by A1, Def9; :: thesis: verum

end;

assume [a,b] in f " ; :: thesis: [a,b] in g
then [a,b] in f ~ by A1, Def9;
then A13: [b,a] in f by RELAT_1:def 7;
then A14: b in dom f by RELAT_1:def 4;
then a = f . b by A13, Def4;
then ( a in rng f & b = g . a ) by A11, A14;
hence [a,b] in g by A10, Def4; :: thesis: verum