let X be non empty set ; :: thesis: card (product <*X*>) = card X

consider I being Function of X,(product <*X*>) such that

A1: ( I is one-to-one & I is onto & ( for x being object st x in X holds

I . x = <*x*> ) ) by PRVECT_3:4;

not {} in rng <*X*>

then A2: dom I = X by FUNCT_2:def 1;

rng I = product <*X*> by A1, FUNCT_2:def 3;

hence card X = card (product <*X*>) by CARD_1:5, A1, A2, WELLORD2:def 4; :: thesis: verum

consider I being Function of X,(product <*X*>) such that

A1: ( I is one-to-one & I is onto & ( for x being object st x in X holds

I . x = <*x*> ) ) by PRVECT_3:4;

not {} in rng <*X*>

proof

then
product <*X*> <> {}
by CARD_3:26;
assume
{} in rng <*X*>
; :: thesis: contradiction

then {} in {X} by FINSEQ_1:39;

hence contradiction by TARSKI:def 1; :: thesis: verum

end;then {} in {X} by FINSEQ_1:39;

hence contradiction by TARSKI:def 1; :: thesis: verum

then A2: dom I = X by FUNCT_2:def 1;

rng I = product <*X*> by A1, FUNCT_2:def 3;

hence card X = card (product <*X*>) by CARD_1:5, A1, A2, WELLORD2:def 4; :: thesis: verum