let X be non empty set ; for D being Function st dom D = {1} & D . 1 = X holds
ex I being Function of X,(product D) st
( I is one-to-one & I is onto & ( for x being object st x in X holds
I . x = <*x*> ) )
let D be Function; ( dom D = {1} & D . 1 = X implies ex I being Function of X,(product D) st
( I is one-to-one & I is onto & ( for x being object st x in X holds
I . x = <*x*> ) ) )
assume A1:
( dom D = {1} & D . 1 = X )
; ex I being Function of X,(product D) st
( I is one-to-one & I is onto & ( for x being object st x in X holds
I . x = <*x*> ) )
defpred S1[ object , object ] means $2 = <*$1*>;
A2:
for x being object st x in X holds
ex z being object st
( z in product D & S1[x,z] )
consider I being Function of X,(product D) such that
A5:
for x being object st x in X holds
S1[x,I . x]
from FUNCT_2:sch 1(A2);
then A6:
product D <> {}
by CARD_3:26;
then A8:
I is one-to-one
by A6, FUNCT_2:19;
now for w being object st w in product D holds
w in rng Ilet w be
object ;
( w in product D implies w in rng I )assume
w in product D
;
w in rng Ithen consider g being
Function such that A9:
(
w = g &
dom g = dom D & ( for
i being
object st
i in dom D holds
g . i in D . i ) )
by CARD_3:def 5;
reconsider g =
g as
FinSequence by A1, A9, FINSEQ_1:2, FINSEQ_1:def 2;
set x =
g . 1;
A10:
len g = 1
by A1, A9, FINSEQ_1:2, FINSEQ_1:def 3;
1
in dom D
by A1, TARSKI:def 1;
then A11:
(
g . 1
in X &
w = <*(g . 1)*> )
by A9, A10, A1, FINSEQ_1:40;
then
w = I . (g . 1)
by A5;
hence
w in rng I
by A11, A6, FUNCT_2:112;
verum end;
then
product D c= rng I
by TARSKI:def 3;
then
product D = rng I
by XBOOLE_0:def 10;
then
I is onto
by FUNCT_2:def 3;
hence
ex I being Function of X,(product D) st
( I is one-to-one & I is onto & ( for x being object st x in X holds
I . x = <*x*> ) )
by A5, A8; verum