let D be non empty set ; :: thesis: ( 1 -tuples_on D,D are_equipotent & card (1 -tuples_on D) = card D )
deffunc H1( object ) -> set = <*$1*>;
consider f being Function such that
A1: ( dom f = D & ( for x being object st x in D holds
f . x = H1(x) ) ) from FUNCT_1:sch 3();
 D,1 -tuples_on D are_equipotent
proof
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 )
proof
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;
thus dom f = D by A1; :: thesis: 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
proof
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;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in 1 -tuples_on D or x in 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;
hence ( 1 -tuples_on D,D are_equipotent & card (1 -tuples_on D) = card D ) by CARD_1:5; :: thesis: verum