let f be Function-yielding 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 ) )
set h0 = the Element of product (doms f);
A1: dom (doms f) = dom f by Def1;
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 :: thesis: not {} in rng (doms f)

assume {} in rng (doms f) ; :: thesis: contradiction
then consider x being object such that
A3: x in dom (doms f) and
A4: {} = (doms f) . x by FUNCT_1:def 3;
A5: x in dom f by A3, Def1;
reconsider g = f . x as Function ;
A6: x in dom f by A5;
then A7: g in rng f by FUNCT_1:def 3;
{} = dom g by A4, A6, Th18;
hence contradiction by A2, A7, RELAT_1:41; :: thesis: verum

end;

then product (doms f) <> {} by CARD_3:26;
then consider h being Function such that
the Element of product (doms f) = h and
dom h = dom (doms f) and
A8: for x being object 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 Def6;
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₁( object ) -> set = h . $1;
assume A10: for x, y being object 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 4 :: 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 object such that
A11: ( z in dom f & g = f . z ) by FUNCT_1:def 3;
defpred S₁[ object ] means $1 = z;
let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom g or not y in dom g or not g . x = g . y or x = y )
deffunc H₂( object ) -> object = x;
consider h1 being Function such that
A12: ( dom h1 = dom f & ( for a being object st a in dom 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 :: thesis: for a being object st a in dom (doms f) holds
h1 . a in (doms f) . a

let a be object ; :: 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, Th18; :: 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 = dom f and
A21: for x being object st x in dom g1 holds
g1 . x = (uncurry f) . (x,(h1 . x)) by Def6;
defpred S₂[ object ] means $1 = z;
deffunc H₃( object ) -> set = h . $1;
deffunc H₄( object ) -> object = y;
consider h2 being Function such that
A22: ( dom h2 = dom f & ( for a being object st a in dom f holds
( ( S₂[a] implies h2 . a = H₄(a) ) & ( not S₂[a] implies h2 . a = H₃(a) ) ) ) ) from PARTFUN1:sch 1();

now :: thesis: for a being object st a in dom (doms f) holds
h2 . a in (doms f) . a

let a be object ; :: 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, Th18; :: 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 = dom f and
A28: for x being object st x in dom g2 holds
g2 . x = (uncurry f) . (x,(h2 . x)) by Def6;

now :: thesis: for a being object st a in dom f holds
g1 . a = g2 . a

let a be object ; :: thesis: ( a in dom f implies g1 . b₁ = g2 . b₁ )
assume A29: a in dom 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:38;
h2 . a = y by A22, A29, A33;
hence g1 . a = g2 . a by A11, A14, A15, A30, A33, A34, FUNCT_5:38; :: thesis: verum

end;

end;

end;

then g1 = g2 by A20, A27;
then A35: h1 = h2 by A9, A10, A18, A19, A25, A26;
A36: z in dom f by A11;
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, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom (Frege f) or not y in dom (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 object 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 object 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 = dom f & ( for x being object st x in dom h2 holds
h2 . x = (uncurry f) . (x,(g2 . x)) ) ) by A9, A39, A41, Def6;
consider h1 being Function such that
A49: (Frege f) . g1 = h1 and
A50: ( dom h1 = dom f & ( for x being object st x in dom h1 holds
h1 . x = (uncurry f) . (x,(g1 . x)) ) ) by A9, A38, A44, Def6;

now :: thesis: for a being object st a in dom f holds
g1 . a = g2 . a

let a be object ; :: thesis: ( a in dom f implies g1 . a = g2 . a )
assume A51: a in dom f ; :: thesis: g1 . a = g2 . a
reconsider g = f . a as Function ;
A52: a in dom f by A51;
then A53: dom g = (doms f) . a by Th18;
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:38;
g in rng f by A52, FUNCT_1:def 3;
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:38;
hence g1 . a = g2 . a by A40, A44, A41, A49, A47, A55, A54, A56, A57; :: thesis: verum

end;

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