deffunc H1( Function) -> object = [($1 . 1),($1 . 2)];
let X, Y be set ; :: thesis: ( product <*X,Y*>,[:X,Y:] are_equipotent & card (product <*X,Y*>) = (card X) *` (card Y) )
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 = H1(g) ) ) from FUNCT_5:sch 1();
 A2: <*X,Y*> . 2 = Y by FINSEQ_1:44;
A3: dom <*X,Y*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89;
A4: <*X,Y*> . 1 = X by FINSEQ_1:44;
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 object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume that
A5: x1 in dom f and
A6: x2 in dom f and
A7: f . x1 = f . x2 ; :: thesis: x1 = x2
consider g2 being Function such that
A8: x2 = g2 and
A9: dom g2 = dom <*X,Y*> and
for y being object st y in dom <*X,Y*> holds
g2 . y in <*X,Y*> . y by A1, A6, CARD_3:def 5;
consider g1 being Function such that
A10: x1 = g1 and
A11: dom g1 = dom <*X,Y*> and
for y being object st y in dom <*X,Y*> holds
g1 . y in <*X,Y*> . y by A5, A1, CARD_3:def 5;
A12: [(g1 . 1),(g1 . 2)] = f . x1 by A1, A5, A10
.= [(g2 . 1),(g2 . 2)] by A1, A6, A7, A8 ;
now :: thesis: for z being object st z in {1,2} holds
g1 . z = g2 . z
let z be object ; :: 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 A12, XTUPLE_0:1; :: thesis: verum
end;
hence x1 = x2 by A3, A10, A11, A8, A9, FUNCT_1:2; :: 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 object ; :: 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 object such that
A13: t in dom f and
A14: z = f . t by FUNCT_1:def 3;
consider g being Function such that
A15: t = g and
dom g = dom <*X,Y*> and
A16: for y being object st y in dom <*X,Y*> holds
g . y in <*X,Y*> . y by A1, A13, CARD_3:def 5;
1 in {1,2} by TARSKI:def 2;
then A17: g . 1 in X by A3, A4, A16;
2 in {1,2} by TARSKI:def 2;
then A18: g . 2 in Y by A3, A2, A16;
z = [(g . 1),(g . 2)] by A1, A13, A14, A15;
hence z in [:X,Y:] by A17, A18, ZFMISC_1:87; :: thesis: verum
end;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in [:X,Y:] or z in proj2 f )
set g = <*(z `1),(z `2)*>;
A19: <*(z `1),(z `2)*> . 1 = z `1 by FINSEQ_1:44;
A20: <*(z `1),(z `2)*> . 2 = z `2 by FINSEQ_1:44;
assume A21: z in [:X,Y:] ; :: thesis: z in proj2 f
then A22: z `2 in Y by MCART_1:10;
z `1 in X by A21, MCART_1:10;
then A23: <*(z `1),(z `2)*> in product <*X,Y*> by A22, FINSEQ_3:124;
z = [(z `1),(z `2)] by A21, MCART_1:21;
then f . <*(z `1),(z `2)*> = z by A23, A1, A19, A20;
hence z in proj2 f by A1, A23, FUNCT_1:def 3; :: thesis: verum
end;
hence card (product <*X,Y*>) = card [:X,Y:] by CARD_1:5
.= card [:(card X),(card Y):] by CARD_2:7
.= (card X) *` (card Y) by CARD_2:def 2 ;
:: thesis: verum