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

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