let D be non empty set ; :: thesis: ( 1 -tuples_on D,D are_equipotent & card (1 -tuples_on D) = card D )

deffunc H_{1}( object ) -> set = <*$1*>;

consider f being Function such that

A1: ( dom f = D & ( for x being object st x in D holds

f . x = H_{1}(x) ) )
from FUNCT_1:sch 3();

D,1 -tuples_on D are_equipotent

deffunc H

consider f being Function such that

A1: ( dom f = D & ( for x being object st x in D holds

f . x = H

D,1 -tuples_on D are_equipotent

proof

hence
( 1 -tuples_on D,D are_equipotent & card (1 -tuples_on D) = card D )
by CARD_1:5; :: thesis: verum
take
f
; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & dom f = D & rng f = 1 -tuples_on D )

thus f is one-to-one :: thesis: ( dom f = D & rng f = 1 -tuples_on D )

thus rng f c= 1 -tuples_on D :: according to XBOOLE_0:def 10 :: thesis: 1 -tuples_on D c= rng f

assume x in 1 -tuples_on D ; :: thesis: x in rng f

then reconsider y = x as Element of 1 -tuples_on D ;

consider z being Element of D such that

A5: y = <*z*> by FINSEQ_2:97;

x = f . z by A1, A5;

hence x in rng f by A1, FUNCT_1:def 3; :: thesis: verum

end;thus f is one-to-one :: thesis: ( dom f = D & rng f = 1 -tuples_on D )

proof

thus
dom f = D
by A1; :: thesis: rng f = 1 -tuples_on D
let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )

assume ( x in dom f & y in dom f ) ; :: thesis: ( not f . x = f . y or x = y )

then A2: ( f . x = <*x*> & f . y = <*y*> ) by A1;

<*x*> . 1 = x by FINSEQ_1:def 8;

hence ( not f . x = f . y or x = y ) by A2, FINSEQ_1:def 8; :: thesis: verum

end;assume ( x in dom f & y in dom f ) ; :: thesis: ( not f . x = f . y or x = y )

then A2: ( f . x = <*x*> & f . y = <*y*> ) by A1;

<*x*> . 1 = x by FINSEQ_1:def 8;

hence ( not f . x = f . y or x = y ) by A2, FINSEQ_1:def 8; :: thesis: verum

thus rng f c= 1 -tuples_on D :: according to XBOOLE_0:def 10 :: thesis: 1 -tuples_on D c= rng f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in 1 -tuples_on D or x in rng f )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in 1 -tuples_on D )

assume x in rng f ; :: thesis: x in 1 -tuples_on D

then consider y being object such that

A3: y in dom f and

A4: x = f . y by FUNCT_1:def 3;

reconsider y = y as Element of D by A1, A3;

x = <*y*> by A1, A4;

then x in { <*d*> where d is Element of D : verum } ;

hence x in 1 -tuples_on D by FINSEQ_2:96; :: thesis: verum

end;assume x in rng f ; :: thesis: x in 1 -tuples_on D

then consider y being object such that

A3: y in dom f and

A4: x = f . y by FUNCT_1:def 3;

reconsider y = y as Element of D by A1, A3;

x = <*y*> by A1, A4;

then x in { <*d*> where d is Element of D : verum } ;

hence x in 1 -tuples_on D by FINSEQ_2:96; :: thesis: verum

assume x in 1 -tuples_on D ; :: thesis: x in rng f

then reconsider y = x as Element of 1 -tuples_on D ;

consider z being Element of D such that

A5: y = <*z*> by FINSEQ_2:97;

x = f . z by A1, A5;

hence x in rng f by A1, FUNCT_1:def 3; :: thesis: verum