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 ) )
consider h0 being Element of product (doms f);
A1: dom (doms f) = f " (SubFuncs (rng f)) by Def2;
assume A2: 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
A3: x in dom (doms f) and
A4: {} = (doms f) . x by FUNCT_1:def 5;
A5: x in f " (SubFuncs (rng f)) by A3, Def2;
then f . x in SubFuncs (rng f) by FUNCT_1:def 13;
then reconsider g = f . x as Function by Def1;
A6: x in dom f by A5, FUNCT_1:def 13;
then A7: g in rng f by FUNCT_1:def 5;
{} = dom g by A4, A6, Th31;
hence contradiction by A2, A7, RELAT_1:64; :: thesis: verum

end;

then product (doms f) <> {} by CARD_3:37;
then consider h being Function such that
h0 = h and
dom h = dom (doms f) and
A8: for x being set st x in dom (doms f) holds
h . x in (doms f) . x by CARD_3:def 5;
A9: dom (Frege f) = product (doms f) by 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

deffunc H₁( set ) -> set = h . $1;
assume A10: 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
A11: ( z in dom f & g = f . z ) by FUNCT_1:def 5;
defpred S₁[ set ] means $1 = z;
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;
consider h1 being Function such that
A12: ( 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();
assume that
A13: x in dom g and
A14: y in dom g and
A15: 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 A16: a in dom (doms f) ; :: thesis: h1 . a in (doms f) . a
then A17: ( a <> z implies h1 . a = h . a ) by A1, A12;
( a = z implies h1 . a = x ) by A1, A12, A16;
hence h1 . a in (doms f) . a by A8, A11, A13, A16, A17, Th31; :: thesis: verum

end;

then A18: h1 in product (doms f) by A1, A12, CARD_3:def 5;
then consider g1 being Function such that
A19: (Frege f) . h1 = g1 and
A20: dom g1 = f " (SubFuncs (rng f)) and
A21: for x being set st x in dom g1 holds
g1 . x = (uncurry f) . (x,(h1 . x)) by Def7;
defpred S₂[ set ] means $1 = z;
deffunc H₃( set ) -> set = h . $1;
deffunc H₄( set ) -> set = y;
consider h2 being Function such that
A22: ( 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();

now

let a be set ; :: thesis: ( a in dom (doms f) implies h2 . a in (doms f) . a )
assume A23: a in dom (doms f) ; :: thesis: h2 . a in (doms f) . a
then A24: ( a <> z implies h2 . a = h . a ) by A1, A22;
( a = z implies h2 . a = y ) by A1, A22, A23;
hence h2 . a in (doms f) . a by A8, A11, A14, A23, A24, Th31; :: thesis: verum

end;

then A25: h2 in product (doms f) by A1, A22, CARD_3:def 5;
then consider g2 being Function such that
A26: (Frege f) . h2 = g2 and
A27: dom g2 = f " (SubFuncs (rng f)) and
A28: 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 A29: a in f " (SubFuncs (rng f)) ; :: thesis: g1 . b₁ = g2 . b₁
then A30: g2 . a = (uncurry f) . (a,(h2 . a)) by A27, A28;
A31: g1 . a = (uncurry f) . (a,(h1 . a)) by A20, A21, A29;

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

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

then h1 . a = h . a by A12, A29;
hence g1 . a = g2 . a by A22, A29, A30, A31, A32; :: thesis: verum

end;

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

then h1 . a = x by A12, A29;
then A34: g1 . a = g . x by A11, A13, A31, A33, FUNCT_5:45;
h2 . a = y by A22, A29, A33;
hence g1 . a = g2 . a by A11, A14, A15, A30, A33, A34, FUNCT_5:45; :: thesis: verum

end;

end;

end;

then g1 = g2 by A20, A27, FUNCT_1:9;
then A35: h1 = h2 by A9, A10, A18, A19, A25, A26;
g in rng f by A11, FUNCT_1:def 5;
then g in SubFuncs (rng f) by Def1;
then A36: z in f " (SubFuncs (rng f)) by A11, FUNCT_1:def 13;
then h1 . z = x by A12;
hence x = y by A36, A22, A35; :: thesis: verum

end;

assume A37: 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 that
A38: x in dom (Frege f) and
A39: y in dom (Frege f) and
A40: (Frege f) . x = (Frege f) . y ; :: thesis: x = y
consider g2 being Function such that
A41: y = g2 and
A42: dom g2 = dom (doms f) and
A43: for x being set st x in dom (doms f) holds
g2 . x in (doms f) . x by A9, A39, CARD_3:def 5;
consider g1 being Function such that
A44: x = g1 and
A45: dom g1 = dom (doms f) and
A46: for x being set st x in dom (doms f) holds
g1 . x in (doms f) . x by A9, A38, CARD_3:def 5;
consider h2 being Function such that
A47: (Frege f) . g2 = h2 and
A48: ( dom h2 = f " (SubFuncs (rng f)) & ( for x being set st x in dom h2 holds
h2 . x = (uncurry f) . (x,(g2 . x)) ) ) by A9, A39, A41, Def7;
consider h1 being Function such that
A49: (Frege f) . g1 = h1 and
A50: ( dom h1 = f " (SubFuncs (rng f)) & ( for x being set st x in dom h1 holds
h1 . x = (uncurry f) . (x,(g1 . x)) ) ) by A9, A38, A44, Def7;

now

let a be set ; :: thesis: ( a in f " (SubFuncs (rng f)) implies g1 . a = g2 . a )
assume A51: a in f " (SubFuncs (rng f)) ; :: thesis: g1 . a = g2 . a
then f . a in SubFuncs (rng f) by FUNCT_1:def 13;
then reconsider g = f . a as Function by Def1;
A52: a in dom f by A51, FUNCT_1:def 13;
then A53: dom g = (doms f) . a by Th31;
then A54: g2 . a in dom g by A1, A43, A51;
A55: g1 . a in dom g by A1, A46, A51, A53;
h2 . a = (uncurry f) . (a,(g2 . a)) by A48, A51;
then A56: h2 . a = g . (g2 . a) by A52, A54, FUNCT_5:45;
g in rng f by A52, FUNCT_1:def 5;
then A57: g is one-to-one by A37;
h1 . a = (uncurry f) . (a,(g1 . a)) by A50, A51;
then h1 . a = g . (g1 . a) by A52, A55, FUNCT_5:45;
hence g1 . a = g2 . a by A40, A44, A41, A49, A47, A55, A54, A56, A57, FUNCT_1:def 8; :: thesis: verum

end;

hence x = y by A1, A44, A45, A41, A42, FUNCT_1:9; :: thesis: verum