let X be non empty set ; :: thesis: 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 set st x in X holds
I . x = <*x*> ) )
let D be Function; :: thesis: ( 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 set st x in X holds
I . x = <*x*> ) ) )
assume AS: ( dom D = {1} & D . 1 = X ) ; :: thesis: ex I being Function of X,(product D) st
( I is one-to-one & I is onto & ( for x being set st x in X holds
I . x = <*x*> ) )
defpred S₁[ set , set ] means $2 = <*$1*>;
P1: for x being set st x in X holds
ex z being set st
( z in product D & S₁[x,z] )

proof

let x be set ; :: thesis: ( x in X implies ex z being set st
( z in product D & S₁[x,z] ) )
assume AS0: x in X ; :: thesis: ex z being set st
( z in product D & S₁[x,z] )
X0: dom <*x*> = Seg (len <*x*>) by FINSEQ_1:def 3
.= {1} by FINSEQ_1:4, FINSEQ_1:57 ;

now

let i be set ; :: thesis: ( i in dom <*x*> implies <*x*> . i in D . i )
assume i in dom <*x*> ; :: thesis: <*x*> . i in D . i
then i = 1 by X0, TARSKI:def 1;
hence <*x*> . i in D . i by AS, AS0, FINSEQ_1:57; :: thesis: verum

end;

then <*x*> in product D by X0, AS, CARD_3:18;
hence ex z being set st
( z in product D & S₁[x,z] ) ; :: thesis: verum

end;

consider I being Function of X,(product D) such that
P2: for x being set st x in X holds
S₁[x,I . x] from FUNCT_2:sch 1(P1);

now

assume {} in rng D ; :: thesis: contradiction
then ex x being set st
( x in dom D & D . x = {} ) by FUNCT_1:def 5;
hence contradiction by AS, TARSKI:def 1; :: thesis: verum

end;

then A6: product D <> {} by CARD_3:37;

now

let z1, z2 be set ; :: thesis: ( z1 in X & z2 in X & I . z1 = I . z2 implies z1 = z2 )
assume P3: ( z1 in X & z2 in X & I . z1 = I . z2 ) ; :: thesis: z1 = z2
<*z1*> = I . z1 by P2, P3
.= <*z2*> by P2, P3 ;
hence z1 = z2 by FINSEQ_1:97; :: thesis: verum

end;

then P3: I is one-to-one by A6, FUNCT_2:25;

now

let w be set ; :: thesis: ( w in product D implies w in rng I )
assume w in product D ; :: thesis: w in rng I
then consider g being Function such that
X1: ( w = g & dom g = dom D & ( for i being set st i in dom D holds
g . i in D . i ) ) by CARD_3:def 5;
reconsider g = g as FinSequence by AS, X1, FINSEQ_1:4, FINSEQ_1:def 2;
set x = g . 1;
X3: len g = 1 by AS, X1, FINSEQ_1:4, FINSEQ_1:def 3;
1 in dom D by AS, TARSKI:def 1;
then P40: ( g . 1 in X & w = <*(g . 1)*> ) by X1, X3, AS, FINSEQ_1:57;
then w = I . (g . 1) by P2;
hence w in rng I by P40, A6, FUNCT_2:189; :: thesis: 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 set st x in X holds
I . x = <*x*> ) ) by P2, P3; :: thesis: verum