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:94
.= {{}} ;
hence i -tuples_on D is product-like by CARD_3:10; :: thesis: verum

end;

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

then A1: i -tuples_on D = {} by Th117;
take f = 0 .--> {}; :: according to CARD_3:def 13 :: thesis: i -tuples_on D = product f
rng f = {{}} by FUNCOP_1:8;
then {} in rng f by TARSKI:def 1;
hence i -tuples_on D = product f by A1, CARD_3:26; :: 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 13 :: 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:77; :: according to XBOOLE_0:def 10 :: thesis: product (product" (i -tuples_on D)) c= i -tuples_on D
let x be object ; :: 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 object st z in dom (product" (i -tuples_on D)) holds
g . z in (product" (i -tuples_on D)) . z by CARD_3:def 5;
set s = the Element of i -tuples_on D;
the Element of i -tuples_on D in i -tuples_on D ;
then consider t being Element of D * such that
A5: the Element of i -tuples_on D = t and
A6: len t = i ;
A7: dom g = DOM (i -tuples_on D) by A3, CARD_3:def 12
.= dom the Element of i -tuples_on D by CARD_3:108 ;
dom the Element of i -tuples_on D = Seg (len t) by A5, FINSEQ_1:def 3;
then A8: g is FinSequence by A7, FINSEQ_1:def 2;
rng g c= D

proof

let y be object ; :: 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 object such that
A9: a in dom g and
A10: g . a = y by FUNCT_1:def 3;
reconsider a = a as set by TARSKI:1;
g . a in (product" (i -tuples_on D)) . a by A3, A4, A9;
then g . a in pi ((i -tuples_on D),a) by A3, A9, CARD_3:def 12;
then consider f being Function such that
A11: f in i -tuples_on D and
A12: g . a = f . a by CARD_3:def 6;
consider w being Element of D * such that
A13: f = w and
len w = i by A11;
dom g = dom w by A7, A11, A13, CARD_3:def 10;
then w . a in rng w by A9, FUNCT_1:def 3;
hence y in D by A10, A12, A13; :: thesis: verum

end;

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

end;

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

end;

end;