let f be Function-yielding Function; ( 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
; ( Frege f is one-to-one iff for g being Function st g in rng f holds
g is one-to-one )
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 )
( ( for g being Function st g in rng f holds
g is one-to-one ) implies Frege f is one-to-one )proof
deffunc H1(
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
;
FUNCT_1:def 4 for g being Function st g in rng f holds
g is one-to-one
let g be
Function;
( g in rng f implies g is one-to-one )
assume
g in rng f
;
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 S1[
object ]
means $1
= z;
let x,
y be
object ;
FUNCT_1:def 4 ( not x in dom g or not y in dom g or not g . x = g . y or x = y )
deffunc H2(
object )
-> object =
x;
consider h1 being
Function such that A12:
(
dom h1 = dom f & ( for
a being
object st
a in dom f holds
( (
S1[
a] implies
h1 . a = H2(
a) ) & ( not
S1[
a] implies
h1 . a = H1(
a) ) ) ) )
from PARTFUN1:sch 1();
assume that A13:
x in dom g
and A14:
y in dom g
and A15:
g . x = g . y
;
x = y
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 S2[
object ]
means $1
= z;
deffunc H3(
object )
-> set =
h . $1;
deffunc H4(
object )
-> object =
y;
consider h2 being
Function such that A22:
(
dom h2 = dom f & ( for
a being
object st
a in dom f holds
( (
S2[
a] implies
h2 . a = H4(
a) ) & ( not
S2[
a] implies
h2 . a = H3(
a) ) ) ) )
from PARTFUN1:sch 1();
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 for a being object st a in dom f holds
g1 . a = g2 . alet a be
object ;
( a in dom f implies g1 . b1 = g2 . b1 )assume A29:
a in dom f
;
g1 . b1 = g2 . b1then 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 A33:
a = z
;
g1 . b1 = g2 . b1then
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;
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;
verum
end;
assume A37:
for g being Function st g in rng f holds
g is one-to-one
; Frege f is one-to-one
let x, y be object ; FUNCT_1:def 4 ( 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
; 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 for a being object st a in dom f holds
g1 . a = g2 . alet a be
object ;
( a in dom f implies g1 . a = g2 . a )assume A51:
a in dom f
;
g1 . a = g2 . areconsider 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;
verum end;
hence
x = y
by A1, A44, A45, A41, A42, FUNCT_1:2; verum