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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (product p) where p is Element of P * : verum } or x in bool (X *) )
reconsider xx = x as set by TARSKI:1;
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 ;
xx c= X *

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in xx or y in X * )
assume y in xx ; :: thesis: y in 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;
dom p = Seg (len p) by FINSEQ_1:def 3;
then A5: y is 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 y is FinSequence of X by A2, A5, 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 4 :: 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 object ; :: 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;
A9: rng x c= X ;
union P = X by EQREL_1:def 4;
then consider p being Function such that
A10: dom p = dom x and
A11: rng p c= P and
A12: x in product p by A9, Th5;
dom p = Seg (len x) by A10, FINSEQ_1:def 3;
then reconsider p = p as FinSequence by FINSEQ_1:def 2;
reconsider p = p as FinSequence of P by A11, 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 A12, 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
A13: A = product p ;
thus A <> {} by A13; :: 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
A14: B = product q ;
assume A15: A <> B ; :: thesis: A misses B
assume A meets B ; :: thesis: contradiction
then consider x being object such that
A16: x in A and
A17: x in B by XBOOLE_0:3;
consider f being Function such that
A18: x = f and
A19: dom f = dom p and
A20: for z being object st z in dom p holds
f . z in p . z by A13, A16, CARD_3:def 5;
A21: 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 A14, A17, 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 A22: z in dom p ; :: thesis: p . z = q . z
then A23: f . z in p . z by A20;
A24: f . z in q . z by A18, A19, A21, A22;
A25: p . z in rng p by A22, FUNCT_1:def 3;
A26: q . z in rng q by A18, A19, A21, A22, FUNCT_1:def 3;
A27: p . z meets q . z by A23, A24, XBOOLE_0:3;
A28: p . z in P by A25;
q . z in P by A26;
hence p . z = q . z by A27, A28, EQREL_1:def 4; :: thesis: verum

end;

hence contradiction by A13, A14, A15, A18, A19, A21, FUNCT_1:2; :: thesis: verum

end;

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