let H, K be non empty finite set ; :: thesis: card (product <*H,K*>) = (card H) * (card K)
consider I being Function of [:H,K:],(product <*H,K*>) such that
A1: ( I is one-to-one & I is onto & ( for x, y being object st x in H & y in K holds
I . (x,y) = <*x,y*> ) ) by PRVECT_3:5;
A2: dom I = [:H,K:] by FUNCT_2:def 1;
rng I = product <*H,K*> by FUNCT_2:def 3, A1;
then card [:H,K:] = card (product <*H,K*>) by CARD_1:5, A1, A2, WELLORD2:def 4;
hence card (product <*H,K*>) = (card H) * (card K) by CARD_2:46; :: thesis: verum