let X be set ; :: thesis: for x being object holds card (X --> x) = card X
let x be object ; :: thesis: card (X --> x) = card X
deffunc H1( object ) -> object = [$1,x];
consider f being Function such that
A1: ( dom f = X & ( for z being object st z in X holds
f . z = H1(z) ) ) from FUNCT_1:sch 3();
now :: thesis: for y being object holds
( ( y in rng f implies y in X --> x ) & ( y in X --> x implies y in rng f ) )
let y be object ; :: thesis: ( ( y in rng f implies y in X --> x ) & ( y in X --> x implies y in rng f ) )
hereby :: thesis: ( y in X --> x implies y in rng f )
assume y in rng f ; :: thesis: y in X --> x
then consider z being object such that
A2: ( z in dom f & f . z = y ) by FUNCT_1:def 3;
A3: y = [z,x] by A1, A2;
( z in X & x in {x} ) by A1, A2, TARSKI:def 1;
then y in [:X,{x}:] by A3, ZFMISC_1:87;
hence y in X --> x by FUNCOP_1:def 2; :: thesis: verum
end;
assume y in X --> x ; :: thesis: y in rng f
then consider z, x0 being object such that
A4: ( z in X & x0 in {x} & y = [z,x0] ) by ZFMISC_1:def 2;
y = [z,x] by A4, TARSKI:def 1
.= f . z by A1, A4 ;
hence y in rng f by A1, A4, FUNCT_1:3; :: thesis: verum
end;
then A5: rng f = X --> x by TARSKI:2;
now :: thesis: for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2
let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume A6: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
then ( f . x1 = [x1,x] & f . x2 = [x2,x] ) by A1;
hence x1 = x2 by A6, XTUPLE_0:1; :: thesis: verum
end;
hence card (X --> x) = card X by A1, A5, FUNCT_1:def 4, CARD_1:70; :: thesis: verum