let f be Function; :: thesis: ( not {} in rng f implies ( Frege f is one-to-one iff for g being Function st g in rng f holds
g is one-to-one ) )
assume A1: not {} in rng f ; :: thesis: ( Frege f is one-to-one iff for g being Function st g in rng f holds
g is one-to-one )

now

assume {} in rng (doms f) ; :: thesis: contradiction
then consider x being set such that
A2: ( x in dom (doms f) & {} = (doms f) . x ) by FUNCT_1:def 5;
x in f " (SubFuncs (rng f)) by A2, Def2;
then A3: ( x in dom f & f . x in SubFuncs (rng f) ) by FUNCT_1:def 13;
then reconsider g = f . x as Function by Def1;
( {} = dom g & g in rng f ) by A2, A3, Th31, FUNCT_1:def 5;
hence contradiction by A1, RELAT_1:64; :: thesis: verum

end;

then A4: product (doms f) <> {} by CARD_3:37;
consider h0 being Element of product (doms f);
consider h being Function such that
A5: ( h0 = h & dom h = dom (doms f) & ( for x being set st x in dom (doms f) holds
h . x in (doms f) . x ) ) by A4, CARD_3:def 5;
A6: ( dom (doms f) = f " (SubFuncs (rng f)) & dom (Frege f) = product (doms f) ) by Def2, Def7;
thus ( Frege f is one-to-one implies for g being Function st g in rng f holds
g is one-to-one ) :: thesis: ( ( for g being Function st g in rng f holds
g is one-to-one ) implies Frege f is one-to-one )

proof

assume A7: for x, y being set st x in dom (Frege f) & y in dom (Frege f) & (Frege f) . x = (Frege f) . y holds
x = y ; :: according to FUNCT_1:def 8 :: thesis: for g being Function st g in rng f holds
g is one-to-one
let g be Function; :: thesis: ( g in rng f implies g is one-to-one )
assume g in rng f ; :: thesis: g is one-to-one
then consider z being set such that
A8: ( z in dom f & g = f . z ) by FUNCT_1:def 5;
g in rng f by A8, FUNCT_1:def 5;
then g in SubFuncs (rng f) by Def1;
then A9: ( dom g = (doms f) . z & z in f " (SubFuncs (rng f)) ) by A8, Th31, FUNCT_1:def 13;
let x be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x in proj1 g or not b₁ in proj1 g or not g . x = g . b₁ or x = b₁ )
let y be set ; :: thesis: ( not x in proj1 g or not y in proj1 g or not g . x = g . y or x = y )
deffunc H₁( set ) -> set = x;
deffunc H₂( set ) -> set = h . $1;
defpred S₁[ set ] means $1 = z;
consider h1 being Function such that
A10: ( dom h1 = f " (SubFuncs (rng f)) & ( for a being set st a in f " (SubFuncs (rng f)) holds
( ( S₁[a] implies h1 . a = H₁(a) ) & ( not S₁[a] implies h1 . a = H₂(a) ) ) ) ) from PARTFUN1:sch 1();
deffunc H₃( set ) -> set = y;
deffunc H₄( set ) -> set = h . $1;
defpred S₂[ set ] means $1 = z;
consider h2 being Function such that
A11: ( dom h2 = f " (SubFuncs (rng f)) & ( for a being set st a in f " (SubFuncs (rng f)) holds
( ( S₂[a] implies h2 . a = H₃(a) ) & ( not S₂[a] implies h2 . a = H₄(a) ) ) ) ) from PARTFUN1:sch 1();
assume A12: ( x in dom g & y in dom g & g . x = g . y ) ; :: thesis: x = y

now

let a be set ; :: thesis: ( a in dom (doms f) implies h1 . a in (doms f) . a )
assume a in dom (doms f) ; :: thesis: h1 . a in (doms f) . a
then ( ( a = z implies h1 . a = x ) & ( a <> z implies h1 . a = h . a ) & h . a in (doms f) . a & ( a = z or a <> z ) ) by A5, A6, A10;
hence h1 . a in (doms f) . a by A8, A12, Th31; :: thesis: verum

end;

then A13: ( h1 in product (doms f) & dom (Frege f) = product (doms f) ) by A6, A10, CARD_3:def 5;
then consider g1 being Function such that
A14: ( (Frege f) . h1 = g1 & dom g1 = f " (SubFuncs (rng f)) & ( for x being set st x in dom g1 holds
g1 . x = (uncurry f) . x,(h1 . x) ) ) by Def7;

now

let a be set ; :: thesis: ( a in dom (doms f) implies h2 . a in (doms f) . a )
assume a in dom (doms f) ; :: thesis: h2 . a in (doms f) . a
then ( ( a = z implies h2 . a = y ) & ( a <> z implies h2 . a = h . a ) & h . a in (doms f) . a & ( a = z or a <> z ) ) by A5, A6, A11;
hence h2 . a in (doms f) . a by A8, A12, Th31; :: thesis: verum

end;

then A15: h2 in product (doms f) by A6, A11, CARD_3:def 5;
then consider g2 being Function such that
A16: ( (Frege f) . h2 = g2 & dom g2 = f " (SubFuncs (rng f)) & ( for x being set st x in dom g2 holds
g2 . x = (uncurry f) . x,(h2 . x) ) ) by Def7;

now

let a be set ; :: thesis: ( a in f " (SubFuncs (rng f)) implies g1 . b₁ = g2 . b₁ )
assume A17: a in f " (SubFuncs (rng f)) ; :: thesis: g1 . b₁ = g2 . b₁
then A18: ( g2 . a = (uncurry f) . a,(h2 . a) & g1 . a = (uncurry f) . a,(h1 . a) ) by A14, A16;

per cases ( a <> z or a = z ) ;

suppose a <> z ; :: thesis: g1 . b₁ = g2 . b₁

then ( h1 . a = h . a & h2 . a = h . a ) by A10, A11, A17;
hence g1 . a = g2 . a by A18; :: thesis: verum

end;

suppose A19: a = z ; :: thesis: g1 . b₁ = g2 . b₁

then ( h1 . a = x & h2 . a = y ) by A10, A11, A17;
then ( g1 . a = g . x & g2 . a = g . y ) by A8, A12, A18, A19, FUNCT_5:45;
hence g1 . a = g2 . a by A12; :: thesis: verum

end;

end;

end;

then g1 = g2 by A14, A16, FUNCT_1:9;
then ( h1 = h2 & h1 . z = x & h2 . z = y ) by A7, A9, A10, A11, A13, A14, A15, A16;
hence x = y ; :: thesis: verum

end;

assume A20: for g being Function st g in rng f holds
g is one-to-one ; :: thesis: Frege f is one-to-one
let x be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x in proj1 (Frege f) or not b₁ in proj1 (Frege f) or not (Frege f) . x = (Frege f) . b₁ or x = b₁ )
let y be set ; :: thesis: ( not x in proj1 (Frege f) or not y in proj1 (Frege f) or not (Frege f) . x = (Frege f) . y or x = y )
assume A21: ( x in dom (Frege f) & y in dom (Frege f) & (Frege f) . x = (Frege f) . y ) ; :: thesis: x = y
then consider g1 being Function such that
A22: ( x = g1 & dom g1 = dom (doms f) & ( for x being set st x in dom (doms f) holds
g1 . x in (doms f) . x ) ) by A6, CARD_3:def 5;
consider g2 being Function such that
A23: ( y = g2 & dom g2 = dom (doms f) & ( for x being set st x in dom (doms f) holds
g2 . x in (doms f) . x ) ) by A6, A21, CARD_3:def 5;
consider h1 being Function such that
A24: ( (Frege f) . g1 = h1 & dom h1 = f " (SubFuncs (rng f)) & ( for x being set st x in dom h1 holds
h1 . x = (uncurry f) . x,(g1 . x) ) ) by A6, A21, A22, Def7;
consider h2 being Function such that
A25: ( (Frege f) . g2 = h2 & dom h2 = f " (SubFuncs (rng f)) & ( for x being set st x in dom h2 holds
h2 . x = (uncurry f) . x,(g2 . x) ) ) by A6, A21, A23, Def7;

now

let a be set ; :: thesis: ( a in f " (SubFuncs (rng f)) implies g1 . a = g2 . a )
assume A26: a in f " (SubFuncs (rng f)) ; :: thesis: g1 . a = g2 . a
then A27: ( f . a in SubFuncs (rng f) & a in dom f ) by FUNCT_1:def 13;
then reconsider g = f . a as Function by Def1;
dom g = (doms f) . a by A27, Th31;
then A28: ( g1 . a in dom g & g2 . a in dom g & h1 . a = (uncurry f) . a,(g1 . a) & h2 . a = (uncurry f) . a,(g2 . a) & g in rng f ) by A6, A22, A23, A24, A25, A26, A27, FUNCT_1:def 5;
then ( h1 . a = g . (g1 . a) & h2 . a = g . (g2 . a) & g is one-to-one ) by A20, A27, FUNCT_5:45;
hence g1 . a = g2 . a by A21, A22, A23, A24, A25, A28, FUNCT_1:def 8; :: thesis: verum

end;

hence x = y by A6, A22, A23, FUNCT_1:9; :: thesis: verum