set S = i -tuples_on D;
per cases
( ( D = {} & i = 0 ) or ( D = {} & i <> 0 ) or D <> {} )
;
suppose
D <> {}
;
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)
;
CARD_3:def 13 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;
XBOOLE_0:def 10 product (product" (i -tuples_on D)) c= i -tuples_on D
let x be
object ;
TARSKI:def 3 ( 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))
;
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 ;
TARSKI:def 3 ( not y in rng g or y in D )
assume
y in rng g
;
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 A14:
w . a in rng w
by A9, FUNCT_1:def 3;
thus
y in D
by A10, A12, A13, A14;
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;
verum
end; hence
i -tuples_on D = product (product" (i -tuples_on D))
;
verum end;