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 object 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 object st x in X holds
I . x = <*x*> ) ) )
assume A1: ( 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 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] )
proof
let x be object ; :: thesis: ( x in X implies ex z being object st
( z in product D & S1[x,z] ) )
assume A3: x in X ; :: thesis: ex z being object st
( z in product D & S1[x,z] )
A4: dom <*x*> = Seg (len <*x*>) by FINSEQ_1:def 3
.= {1} by FINSEQ_1:2, FINSEQ_1:40 ;
now :: thesis: for i being object st i in dom <*x*> holds
<*x*> . i in D . i
let i be object ; :: 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 A4, TARSKI:def 1;
hence <*x*> . i in D . i by A1, A3, FINSEQ_1:40; :: thesis: verum
end;
then <*x*> in product D by A4, A1, CARD_3:9;
hence ex z being object st
( z in product D & S1[x,z] ) ; :: thesis: verum
end;
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);
now :: thesis: not {} in rng D
assume {} in rng D ; :: thesis: contradiction
then ex x being object st
( x in dom D & D . x = {} ) by FUNCT_1:def 3;
hence contradiction by A1, TARSKI:def 1; :: thesis: verum
end;
then A6: product D <> {} by CARD_3:26;
now :: thesis: for z1, z2 being object st z1 in X & z2 in X & I . z1 = I . z2 holds
z1 = z2
let z1, z2 be object ; :: thesis: ( z1 in X & z2 in X & I . z1 = I . z2 implies z1 = z2 )
assume A7: ( z1 in X & z2 in X & I . z1 = I . z2 ) ; :: thesis: z1 = z2
<*z1*> = I . z1 by A5, A7
.= <*z2*> by A5, A7 ;
hence z1 = z2 by FINSEQ_1:76; :: thesis: verum
end;
then A8: I is one-to-one by A6, FUNCT_2:19;
now :: thesis: for w being object st w in product D holds
w in rng I
let w be object ; :: 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
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; :: 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 object st x in X holds
I . x = <*x*> ) ) by A5, A8; :: thesis: verum