let X be non empty set ; for n being Element of NAT
for P being a_partition of X holds { (product p) where p is Element of n -tuples_on P : verum } is a_partition of n -tuples_on X
let n be Element of NAT ; for P being a_partition of X holds { (product p) where p is Element of n -tuples_on P : verum } is a_partition of n -tuples_on X
let P be a_partition of X; { (product p) where p is Element of n -tuples_on P : verum } is a_partition of n -tuples_on X
set nP = n -tuples_on P;
set nX = n -tuples_on X;
set PP = { (product p) where p is Element of n -tuples_on P : verum } ;
{ (product p) where p is Element of n -tuples_on P : verum } c= bool (n -tuples_on X)
then reconsider PP = { (product p) where p is Element of n -tuples_on P : verum } as Subset-Family of (n -tuples_on X) ;
PP is a_partition of n -tuples_on X
proof
thus
union PP c= n -tuples_on X
;
XBOOLE_0:def 10,
EQREL_1:def 4 ( n -tuples_on X c= union PP & ( for b1 being Element of bool (n -tuples_on X) holds
( not b1 in PP or ( not b1 = {} & ( for b2 being Element of bool (n -tuples_on X) holds
( not b2 in PP or b1 = b2 or b1 misses b2 ) ) ) ) ) )
thus
n -tuples_on X c= union PP
for b1 being Element of bool (n -tuples_on X) holds
( not b1 in PP or ( not b1 = {} & ( for b2 being Element of bool (n -tuples_on X) holds
( not b2 in PP or b1 = b2 or b1 misses b2 ) ) ) )
let A be
Subset of
(n -tuples_on X);
( not A in PP or ( not A = {} & ( for b1 being Element of bool (n -tuples_on X) holds
( not b1 in PP or A = b1 or A misses b1 ) ) ) )
assume
A in PP
;
( not A = {} & ( for b1 being Element of bool (n -tuples_on X) holds
( not b1 in PP or A = b1 or A misses b1 ) ) )
then consider p being
Element of
n -tuples_on P such that A17:
A = product p
;
thus
A <> {}
by A17;
for b1 being Element of bool (n -tuples_on X) holds
( not b1 in PP or A = b1 or A misses b1 )
let B be
Subset of
(n -tuples_on X);
( not B in PP or A = B or A misses B )
assume
B in PP
;
( A = B or A misses B )
then consider q being
Element of
n -tuples_on P such that A18:
B = product q
;
assume A19:
A <> B
;
A misses B
assume
A meets B
;
contradiction
then consider x being
object such that A20:
x in A
and A21:
x in B
by XBOOLE_0:3;
consider f being
Function such that A22:
x = f
and A23:
dom f = dom p
and A24:
for
z being
object st
z in dom p holds
f . z in p . z
by A17, A20, CARD_3:def 5;
A25:
ex
g being
Function st
(
x = g &
dom g = dom q & ( for
z being
object st
z in dom q holds
g . z in q . z ) )
by A18, A21, CARD_3:def 5;
now for z being object st z in dom p holds
p . z = q . zlet z be
object ;
( z in dom p implies p . z = q . z )assume A26:
z in dom p
;
p . z = q . zthen A27:
f . z in p . z
by A24;
A28:
f . z in q . z
by A22, A23, A25, A26;
A29:
p . z in rng p
by A26, FUNCT_1:def 3;
A30:
q . z in rng q
by A22, A23, A25, A26, FUNCT_1:def 3;
A31:
p . z meets q . z
by A27, A28, XBOOLE_0:3;
A32:
p . z in P
by A29;
q . z in P
by A30;
hence
p . z = q . z
by A31, A32, EQREL_1:def 4;
verum end;
hence
contradiction
by A17, A18, A19, A22, A23, A25, FUNCT_1:2;
verum
end;
hence
{ (product p) where p is Element of n -tuples_on P : verum } is a_partition of n -tuples_on X
; verum