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*>

proof

assume {} in rng <*X*> ; :: thesis: contradiction
then {} in {X} by FINSEQ_1:39;
hence contradiction by TARSKI:def 1; :: thesis: verum

end;

then product <*X*> <> {} by CARD_3:26;
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