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 object 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 object 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 object 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 object 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 object 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 object holds
( y in rng f & x = g . y iff ( x in dom f & y = f . x ) ) ) )
then A2: g = f ~ by A1, Def5;
hence dom g = rng f by RELAT_1:20; :: thesis: for y, x being object holds
( y in rng f & x = g . y iff ( x in dom f & y = f . x ) )
let y, x be object ; :: 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 )
reconsider y = y as set by TARSKI:1;
y in dom g by A2, A3, RELAT_1:20;
then [y,x] in g by A4, Def2;
then A5: [x,y] in f by A2, RELAT_1:def 7;
hence x in dom f by XTUPLE_0:def 12; :: thesis: y = f . x
hence y = f . x by A5, Def2; :: thesis: verum

end;

assume ( x in dom f & y = f . x ) ; :: thesis: ( y in rng f & x = g . y )
then A6: [x,y] in f by Def2;
hence y in rng f by XTUPLE_0:def 13; :: thesis: x = g . y
then A7: y in dom g by A2, RELAT_1:20;
reconsider x = x as set by TARSKI:1;
[y,x] in g by A2, A6, RELAT_1:def 7;
hence x = g . y by A7, Def2; :: thesis: verum

end;

assume that
A8: dom g = rng f and
A9: for y, x being object holds
( y in rng f & x = g . y iff ( x in dom f & y = f . x ) ) ; :: thesis: g = f "
let a, b be object ; :: 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 A10: [a,b] in g ; :: thesis: [a,b] in f "
reconsider b = b as set by TARSKI:1;
A11: a in dom g by XTUPLE_0:def 12, A10;
then b = g . a by A10, Def2;
then ( b in dom f & a = f . b ) by A8, A9, A11;
then [b,a] in f by Def2;
then [a,b] in f ~ by RELAT_1:def 7;
hence [a,b] in f " by A1, Def5; :: thesis: verum

end;

assume [a,b] in f " ; :: thesis: [a,b] in g
then [a,b] in f ~ by A1, Def5;
then A12: [b,a] in f by RELAT_1:def 7;
then A13: b in dom f by XTUPLE_0:def 12;
reconsider a = a as set by TARSKI:1;
a = f . b by A12, Def2, A13;
then ( a in rng f & b = g . a ) by A9, A13;
hence [a,b] in g by A8, Def2; :: thesis: verum