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 set ; :: 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) )
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 ;
x c= n -tuples_on X

proof

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

proof

let z be set ; :: 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 set such that
A4: ( v in dom p & z = f . v ) by A2, FUNCT_1:def 5;
( p . v in rng p & rng p c= P ) by A4, FUNCT_1:def 5;
then ( p . v in P & P c= bool X ) ;
then ( z in p . v & p . v c= X ) by A2, A4;
hence z in X ; :: thesis: verum

end;

then ( y is FinSequence of X & len y = len p & len p = n ) by A2, A3, FINSEQ_1:def 3, FINSEQ_1:def 4, FINSEQ_1:def 18;
then y is Element of n -tuples_on X by FINSEQ_2:110;
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 6 :: 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 set ; :: 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 ;
( rng x c= X & union P = X ) by EQREL_1:def 6;
then consider p being Function such that
A5: ( dom p = dom x & rng p c= P & x in product p ) by Th6;
A6: dom p = Seg (len x) by A5, FINSEQ_1:def 3;
then reconsider p = p as FinSequence by FINSEQ_1:def 2;
reconsider p = p as FinSequence of P by A5, FINSEQ_1:def 4;
( len p = len x & len x = n ) by A6, FINSEQ_1:def 3, FINSEQ_1:def 18;
then reconsider p = p as Element of n -tuples_on P by FINSEQ_2:110;
product p in PP ;
hence x in union PP by A5, 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
A7: A = product p ;
thus A <> {} by A7; :: 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
A8: B = product q ;
assume A9: A <> B ; :: thesis: A misses B
assume A meets B ; :: thesis: contradiction
then consider x being set such that
A10: ( x in A & x in B ) by XBOOLE_0:3;
consider f being Function such that
A11: ( x = f & dom f = dom p & ( for z being set st z in dom p holds
f . z in p . z ) ) by A7, A10, CARD_3:def 5;
consider g being Function such that
A12: ( x = g & dom g = dom q & ( for z being set st z in dom q holds
g . z in q . z ) ) by A8, A10, CARD_3:def 5;

now

let z be set ; :: thesis: ( z in dom p implies p . z = q . z )
assume z in dom p ; :: thesis: p . z = q . z
then ( f . z in p . z & f . z in q . z & p . z in rng p & q . z in rng q & rng p c= P & rng q c= P ) by A11, A12, FUNCT_1:def 5;
then ( p . z meets q . z & p . z in P & q . z in P & P c= bool X ) by XBOOLE_0:3;
hence p . z = q . z by EQREL_1:def 6; :: thesis: verum

end;

hence contradiction by A7, A8, A9, A11, A12, FUNCT_1:9; :: 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