let X, Y be set ; :: thesis: ( product <*X,Y*>,[:X,Y:] are_equipotent & card (product <*X,Y*>) = (card X) *` (card Y) )
deffunc H<sub>1</sub>( Function) -> set = [($1 . 1),($1 . 2)];
consider f being Function such that
A1: ( dom f = product <*X,Y*> & ( for g being Function st g in product <*X,Y*> holds
f . g = H<sub>1</sub>(g) ) ) from FUNCT_5:sch 1();
A2: ( dom <*X,Y*> = {1,2} & <*X,Y*> . 1 = X & <*X,Y*> . 2 = Y ) by FINSEQ_1:4, FINSEQ_1:61, FINSEQ_3:29;
thus product <*X,Y*>,[:X,Y:] are_equipotent :: thesis: card (product <*X,Y*>) = (card X) *` (card Y)

proof

take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & proj1 f = product <*X,Y*> & proj2 f = [:X,Y:] )
thus f is one-to-one :: thesis: ( proj1 f = product <*X,Y*> & proj2 f = [:X,Y:] )

proof

let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume A3: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
then consider g1 being Function such that
A4: ( x1 = g1 & dom g1 = dom <*X,Y*> & ( for y being set st y in dom <*X,Y*> holds
g1 . y in <*X,Y*> . y ) ) by A1, CARD_3:def 5;
consider g2 being Function such that
A5: ( x2 = g2 & dom g2 = dom <*X,Y*> & ( for y being set st y in dom <*X,Y*> holds
g2 . y in <*X,Y*> . y ) ) by A1, A3, CARD_3:def 5;
A6: [(g1 . 1),(g1 . 2)] = f . x1 by A1, A3, A4
.= [(g2 . 1),(g2 . 2)] by A1, A3, A5 ;

now

let z be set ; :: thesis: ( z in {1,2} implies g1 . z = g2 . z )
assume z in {1,2} ; :: thesis: g1 . z = g2 . z
then ( z = 1 or z = 2 ) by TARSKI:def 2;
hence g1 . z = g2 . z by A6, ZFMISC_1:33; :: thesis: verum

end;

hence x1 = x2 by A2, A4, A5, FUNCT_1:9; :: thesis: verum

end;

thus dom f = product <*X,Y*> by A1; :: thesis: proj2 f = [:X,Y:]
thus rng f c= [:X,Y:] :: according to XBOOLE_0:def 10 :: thesis: [:X,Y:] c= proj2 f

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng f or z in [:X,Y:] )
assume z in rng f ; :: thesis: z in [:X,Y:]
then consider t being set such that
A7: ( t in dom f & z = f . t ) by FUNCT_1:def 5;
consider g being Function such that
A8: ( t = g & dom g = dom <*X,Y*> & ( for y being set st y in dom <*X,Y*> holds
g . y in <*X,Y*> . y ) ) by A1, A7, CARD_3:def 5;
( 1 in {1,2} & 2 in {1,2} ) by TARSKI:def 2;
then ( z = [(g . 1),(g . 2)] & g . 1 in X & g . 2 in Y ) by A1, A2, A7, A8;
hence z in [:X,Y:] by ZFMISC_1:106; :: thesis: verum

end;

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in [:X,Y:] or z in proj2 f )
assume z in [:X,Y:] ; :: thesis: z in proj2 f
then A9: ( z = [(z `1 ),(z `2 )] & z `1 in X & z `2 in Y ) by MCART_1:10, MCART_1:23;
set g = <*(z `1 ),(z `2 )*>;
A10: ( dom <*(z `1 ),(z `2 )*> = {1,2} & <*(z `1 ),(z `2 )*> . 1 = z `1 & <*(z `1 ),(z `2 )*> . 2 = z `2 ) by FINSEQ_1:4, FINSEQ_1:61, FINSEQ_3:29;
A11: <*(z `1 ),(z `2 )*> in product <*X,Y*> by A9, FUNCT_6:2;
then f . <*(z `1 ),(z `2 )*> = z by A1, A9, A10;
hence z in proj2 f by A1, A11, FUNCT_1:def 5; :: thesis: verum

end;

hence card (product <*X,Y*>) = card [:X,Y:] by CARD_1:21
.= card [:(card X),(card Y):] by CARD_2:14
.= (card X) *` (card Y) by CARD_2:def 2 ;
:: thesis: verum