set S = i -tuples_on D;

per cases ( ( D = {} & i = 0 ) or ( D = {} & i <> 0 ) or D <> {} ) ;

suppose ( D = {} & i = 0 ) ; :: thesis: i -tuples_on D is product-like

then i -tuples_on D = {(<*> D)} by FINSEQ_2:112
.= {{} } ;
hence i -tuples_on D is product-like by CARD_3:19; :: thesis: verum

end;

suppose ( D = {} & i <> 0 ) ; :: thesis: i -tuples_on D is product-like

then A1: i -tuples_on D = {} by CATALG_1:7;
take f = 0 .--> {} ; :: according to CARD_3:def 14 :: thesis: i -tuples_on D = product f
rng f = {{} } by FUNCOP_1:14;
then {} in rng f by TARSKI:def 1;
hence i -tuples_on D = product f by A1, CARD_3:37; :: thesis: verum

end;

suppose D <> {} ; :: thesis: i -tuples_on D is product-like

then reconsider D = D as non empty set ;
set S = i -tuples_on D;
take product" (i -tuples_on D) ; :: according to CARD_3:def 14 :: thesis: i -tuples_on D = product (product" (i -tuples_on D))
i -tuples_on D = product (product" (i -tuples_on D))

proof

thus i -tuples_on D c= product (product" (i -tuples_on D)) by CARD_3:94; :: according to XBOOLE_0:def 10 :: thesis: product (product" (i -tuples_on D)) c= i -tuples_on D
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in product (product" (i -tuples_on D)) or x in i -tuples_on D )
assume x in product (product" (i -tuples_on D)) ; :: thesis: x in i -tuples_on D
then consider g being Function such that
A2: x = g and
A3: dom g = dom (product" (i -tuples_on D)) and
A4: for z being set st z in dom (product" (i -tuples_on D)) holds
g . z in (product" (i -tuples_on D)) . z by CARD_3:def 5;
A5: i -tuples_on D = { s where s is Element of D * : len s = i } by FINSEQ_2:def 4;
consider s being Element of i -tuples_on D;
s in i -tuples_on D ;
then consider t being Element of D * such that
A6: s = t and
A7: len t = i by A5;
A8: dom g = DOM (i -tuples_on D) by A3, CARD_3:92
.= dom s by CARD_3:def 12 ;
dom s = Seg (len t) by A6, FINSEQ_1:def 3;
then A9: g is FinSequence by A8, FINSEQ_1:def 2;
rng g c= D

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng g or y in D )
assume y in rng g ; :: thesis: y in D
then consider a being set such that
A10: a in dom g and
A11: g . a = y by FUNCT_1:def 5;
g . a in (product" (i -tuples_on D)) . a by A3, A4, A10;
then g . a in pi (i -tuples_on D),a by A3, A10, CARD_3:def 13;
then consider f being Function such that
A12: f in i -tuples_on D and
A13: g . a = f . a by CARD_3:def 6;
consider w being Element of D * such that
A14: f = w and
len w = i by A5, A12;
dom g = dom w by A8, A12, A14, CARD_3:def 10;
then w . a in rng w by A10, FUNCT_1:def 5;
hence y in D by A11, A13, A14; :: thesis: verum

end;

then reconsider g = g as FinSequence of D by A9, FINSEQ_1:def 4;
A16: g in D * by FINSEQ_1:def 11;
len g = i by A6, A7, A8, FINSEQ_3:31;
hence x in i -tuples_on D by A2, A5, A16; :: thesis: verum

end;

hence i -tuples_on D = product (product" (i -tuples_on D)) ; :: thesis: verum

end;

end;