let X be non empty set ; :: thesis: for P being a_partition of X holds { (product p) where p is Element of P * : verum } is a_partition of X *
let P be a_partition of X; :: thesis: { (product p) where p is Element of P * : verum } is a_partition of X *
set PP = { (product p) where p is Element of P * : verum } ;
{ (product p) where p is Element of P * : verum } c= bool (X * )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (product p) where p is Element of P * : verum } or x in bool (X * ) )
assume x in { (product p) where p is Element of P * : verum } ; :: thesis: x in bool (X * )
then consider p being Element of P * such that
A1: x = product p ;
x c= X *

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in x or y in X * )
assume y in x ; :: thesis: y in 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;
dom p = Seg (len p) by FINSEQ_1:def 3;
then A3: y is 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 by A2, A3, FINSEQ_1:def 4;
hence y in X * by FINSEQ_1:def 11; :: thesis: verum

end;

hence x in bool (X * ) ; :: thesis: verum

end;

then reconsider PP = { (product p) where p is Element of P * : verum } as Subset-Family of (X * ) ;
PP is a_partition of X *

proof

thus union PP c= X * ; :: according to XBOOLE_0:def 10,EQREL_1:def 6 :: thesis: ( X * c= union PP & ( for b₁ being Element of bool (X * ) holds
( not b₁ in PP or ( not b₁ = {} & ( for b₂ being Element of bool (X * ) holds
( not b₂ in PP or b₁ = b₂ or b₁ misses b₂ ) ) ) ) ) )
thus X * c= union PP :: thesis: for b₁ being Element of bool (X * ) holds
( not b₁ in PP or ( not b₁ = {} & ( for b₂ being Element of bool (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 X * or x in union PP )
assume x in X * ; :: thesis: x in union PP
then reconsider x = x as FinSequence of X by FINSEQ_1:def 11;
( 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;
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;
reconsider p = p as Element of P * by FINSEQ_1:def 11;
product p in PP ;
hence x in union PP by A5, TARSKI:def 4; :: thesis: verum

end;

let A be Subset of (X * ); :: thesis: ( not A in PP or ( not A = {} & ( for b₁ being Element of bool (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 (X * ) holds
( not b₁ in PP or A = b₁ or A misses b₁ ) ) )
then consider p being Element of P * such that
A6: A = product p ;
thus A <> {} by A6; :: thesis: for b₁ being Element of bool (X * ) holds
( not b₁ in PP or A = b₁ or A misses b₁ )
let B be Subset of (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 P * such that
A7: B = product q ;
assume A8: A <> B ; :: thesis: A misses B
assume A meets B ; :: thesis: contradiction
then consider x being set such that
A9: ( x in A & x in B ) by XBOOLE_0:3;
consider f being Function such that
A10: ( x = f & dom f = dom p & ( for z being set st z in dom p holds
f . z in p . z ) ) by A6, A9, CARD_3:def 5;
consider g being Function such that
A11: ( x = g & dom g = dom q & ( for z being set st z in dom q holds
g . z in q . z ) ) by A7, A9, 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 A10, A11, 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 A6, A7, A8, A10, A11, FUNCT_1:9; :: thesis: verum

end;

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