let X be non empty set ; 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; { (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 *)
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 *
;
XBOOLE_0:def 10,
EQREL_1:def 4 ( X * c= union PP & ( for b1 being Element of bool (X *) holds
( not b1 in PP or ( not b1 = {} & ( for b2 being Element of bool (X *) holds
( not b2 in PP or b1 = b2 or b1 misses b2 ) ) ) ) ) )
thus
X * c= union PP
for b1 being Element of bool (X *) holds
( not b1 in PP or ( not b1 = {} & ( for b2 being Element of bool (X *) holds
( not b2 in PP or b1 = b2 or b1 misses b2 ) ) ) )
let A be
Subset of
(X *);
( not A in PP or ( not A = {} & ( for b1 being Element of bool (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 (X *) holds
( not b1 in PP or A = b1 or A misses b1 ) ) )
then consider p being
Element of
P * such that A13:
A = product p
;
thus
A <> {}
by A13;
for b1 being Element of bool (X *) holds
( not b1 in PP or A = b1 or A misses b1 )
let B be
Subset of
(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
P * such that A14:
B = product q
;
assume A15:
A <> B
;
A misses B
assume
A meets B
;
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 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 A22:
z in dom p
;
p . z = q . zthen 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;
verum end;
hence
contradiction
by A13, A14, A15, A18, A19, A21, FUNCT_1:2;
verum
end;
hence
{ (product p) where p is Element of P * : verum } is a_partition of X *
; verum