let X be non empty set ; :: thesis: 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 ; :: thesis: 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; :: thesis: { (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)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (product p) where p is Element of n -tuples_on P : verum } or x in bool (n -tuples_on X) )
reconsider xx = x as set by TARSKI:1;
assume x in { (product p) where p is Element of n -tuples_on P : verum } ; :: thesis: x in bool (n -tuples_on X)
then consider p being Element of n -tuples_on P such that
A1: x = product p ;
xx c= n -tuples_on X

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in xx or y in n -tuples_on X )
assume y in xx ; :: thesis: y in n -tuples_on X
then consider f being Function such that
A2: y = f and
A3: dom f = dom p and
A4: for z being object st z in dom p holds
f . z in p . z by A1, CARD_3:def 5;
A5: dom p = Seg (len p) by FINSEQ_1:def 3;
then reconsider y = y as FinSequence by A2, A3, FINSEQ_1:def 2;
rng f c= X

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng f or z in X )
assume z in rng f ; :: thesis: z in X
then consider v being object such that
A6: v in dom p and
A7: z = f . v by A3, FUNCT_1:def 3;
p . v in rng p by A6, FUNCT_1:def 3;
then A8: p . v in P ;
z in p . v by A4, A6, A7;
hence z in X by A8; :: thesis: verum

end;

then A9: y is FinSequence of X by A2, FINSEQ_1:def 4;
A10: len y = len p by A2, A3, A5, FINSEQ_1:def 3;
len p = n by CARD_1:def 7;
then y is Element of n -tuples_on X by A9, A10, FINSEQ_2:92;
hence y in n -tuples_on X ; :: thesis: verum

end;

hence x in bool (n -tuples_on X) ; :: thesis: verum

end;

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 ; :: according to XBOOLE_0:def 10,EQREL_1:def 4 :: thesis: ( n -tuples_on X c= union PP & ( for b₁ being Element of bool (n -tuples_on X) holds
( not b₁ in PP or ( not b₁ = {} & ( for b₂ being Element of bool (n -tuples_on X) holds
( not b₂ in PP or b₁ = b₂ or b₁ misses b₂ ) ) ) ) ) )
thus n -tuples_on X c= union PP :: thesis: for b₁ being Element of bool (n -tuples_on X) holds
( not b₁ in PP or ( not b₁ = {} & ( for b₂ being Element of bool (n -tuples_on X) holds
( not b₂ in PP or b₁ = b₂ or b₁ misses b₂ ) ) ) )

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in n -tuples_on X or x in union PP )
assume x in n -tuples_on X ; :: thesis: x in union PP
then reconsider x = x as Element of n -tuples_on X ;
A11: rng x c= X ;
union P = X by EQREL_1:def 4;
then consider p being Function such that
A12: dom p = dom x and
A13: rng p c= P and
A14: x in product p by A11, Th5;
A15: dom p = Seg (len x) by A12, FINSEQ_1:def 3;
then reconsider p = p as FinSequence by FINSEQ_1:def 2;
reconsider p = p as FinSequence of P by A13, FINSEQ_1:def 4;
A16: len p = len x by A15, FINSEQ_1:def 3;
len x = n by CARD_1:def 7;
then reconsider p = p as Element of n -tuples_on P by A16, FINSEQ_2:92;
product p in PP ;
hence x in union PP by A14, TARSKI:def 4; :: thesis: verum

end;

let A be Subset of (n -tuples_on X); :: thesis: ( not A in PP or ( not A = {} & ( for b₁ being Element of bool (n -tuples_on X) holds
( not b₁ in PP or A = b₁ or A misses b₁ ) ) ) )
assume A in PP ; :: thesis: ( not A = {} & ( for b₁ being Element of bool (n -tuples_on X) holds
( not b₁ in PP or A = b₁ or A misses b₁ ) ) )
then consider p being Element of n -tuples_on P such that
A17: A = product p ;
thus A <> {} by A17; :: thesis: for b₁ being Element of bool (n -tuples_on X) holds
( not b₁ in PP or A = b₁ or A misses b₁ )
let B be Subset of (n -tuples_on X); :: thesis: ( not B in PP or A = B or A misses B )
assume B in PP ; :: thesis: ( 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 ; :: thesis: A misses B
assume A meets B ; :: thesis: 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 :: thesis: for z being object st z in dom p holds
p . z = q . z

let z be object ; :: thesis: ( z in dom p implies p . z = q . z )
assume A26: z in dom p ; :: thesis: p . z = q . z
then 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; :: thesis: verum

end;

hence contradiction by A17, A18, A19, A22, A23, A25, FUNCT_1:2; :: thesis: verum

end;

hence { (product p) where p is Element of n -tuples_on P : verum } is a_partition of n -tuples_on X ; :: thesis: verum